VALLADE Vincent

PhD graduated
Team : MoVe
Departure date : 09/30/2023
https://lip6.fr/Vincent.Vallade

Supervision : Souheib BAARIR, Fabrice KORDON

Co-supervision : SOPENA Julien

Contributions to the parallel resolution of the SAT problem

This thesis presents multiple and orthogonal contributions to improving the parallel resolution of the boolean Satisfiability problem (or SAT problem). An instance of the SAT problem is a boolean formula of a particular form that generally represents the variables and constraints of a real-world problem, such as multi-constraint planning, hardware and software verification, or cryptography. Solving the SAT problem involves determining whether there is a variable assignment that satisfies the formula. An algorithm that can provide an answer to this problem is called a SAT solver. This algorithm has exponential complexity, as the SAT problem was the first to be determined to be NP-complete. Numerous algorithms and heuristics have been developed to speed up the ability to solve this problem, mainly in a sequential context. The ubiquity of multi-core machines has encouraged considerable efforts in parallel solving of the SAT problem. This work is a continuation of those efforts.
In the parallel context, information sharing is a key element of efficiency. It is usually implemented in the form of new lemmas exchanged between the different participants in the parallel solving strategy (i.e., the underlying sequential solvers).
Several strategies for improving this information sharing are presented in this thesis. First, by refining the selection of information to be shared, thanks to the exploitation of the community structure exposed by SAT instances in the industrial world. Second, by adding the ability to reduce the size of the information and avoid sharing redundant information.

Defence : 06/27/2023

Jury members :

Jean-Michel Couvreur, Professeur, Université d’Orléans, LIFO​ [Rapporteur]
Kais Klai, Maître de conférences, Université Sorbonne Paris Nord, LIPN, CNRS​ [Rapporteur]
Hanna Klaudel, Professeure, Université d’Evry, IBISC​
Daniel Le Berre, Professeur, Université d’Artois, CRIL, CNRS​
Souheib Baarir, Enseignant-Chercheur, EPITA​
Fabrice Kordon, Professeur, Sorbonne Université, LIP6, CNRS​
Julien Sopena, Maître de conférences, Sorbonne Université, LIP6, CNRS​

Departure date : 09/30/2023

2020-2023 Publications

Mentions légales
Site map