Forschungsleitung (Direction de recherche) : Souheib BAARIR, Fabrice KORDON

Co-Betreuung : 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.

Publikationen 2020-2023