Homepage of Ludovic Le Frioux

I am a Ph.D. student at LRDE and LIP6 under the direction of Souheib Baarir, and Fabrice Kordon.


My research is about parallel SAT solving. To support that, I develop PaInleSS, a C++ framework simplifying the implementation and evaluation of new concurrent parallel SAT solvers.

Contact Me

Office L6,
EPITA Research and Development Laboratory (LRDE)
14-16 rue Voltaire
94276 Le Kremlin-BicĂȘtre Cedex, France
ludovic~at~lrde.epita.fr
(+33) 1 84 07 16 05

Corridor 25-26, 2nd Floor, Office 231
Laboratoire d'Informatique de Paris 6 (LIP6)
4 place Jussieu
75252 Paris Cedex 05, France
ludovic.le-frioux~at~lip6.fr
(+33) 1 44 27 51 28

Research

Boolean satisfiability (SAT) has been used successfully in many contexts such as planning decision, hardware and software verification, etc. This is due to the capability of modern SAT solvers to solve complex problems involving millions of variables and billions of clauses.

Most SAT solvers have long been sequential and based on the well-known DPLL algorithm. This initial algorithm has been dramatically enhanced by introducing sophisticated heuristics and optimizations: decision heuristics, clauses learning, lazy data structures, etc.

The emergence of many-core machines and cloud computing opens new possibilities in this domain. Two classes of parallel techniques have been developed: competition-based (a.k.a. Portfolio) and cooperation-based (a.k.a. Divide-and-Conquer). In the Portfolio settings, many sequential SAT solvers compete for the solving of the whole problem. The first one to find a solution, or proving the problem to be unsatisfiable ends the computation. Divide-and-Conquer approaches use the guiding path method to decompose, recursively and dynamically, the original problem in sub-problems that are solved separately by sequential solvers. In both approaches, sequential solvers can dynamically share learnt information. Many heuristics exist to improve this sharing by proposing trade-off between gains and overhead.

The goal of my research is to use my knowledge in (distributed) systems to design and implement new algorithms in order to speeding up the resolution time of parallel SAT solvers.

Publications

Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon.
PaInleSS: a Framework for Parallel SAT Solving in Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17), pages 233--250.

Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon.
painless-mapleCOMSPS in Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions, pages 26--27.

Ludovic Le Frioux, Hakan Metin, Souheib Baarir, Maximilien Colange, Julien Sopena, Fabrice Kordon.
painless-mcomsps and painless-mcomsps-sym in Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions, pages 33--34.

Teaching

I am a teaching assistant at EPITA.