Supervision : Souheib BAARIR, Fabrice KORDON

Co-supervision : SOPENA Julien

Sharing groups for parallel SAT solvers

Many industrial problems can be expressed by SAT instances. Due to a large state space size, parallelisation is necessary for the resolution and made possible by the increasing use of massively parallel, also called many-core machines. The purpose of this thesis is to design new algorithms dedicated to this environment, leading to increasing performances for SAT solvers.

2020 Publications

• 2020
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, V. Ganesh, F. Kordon : “Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving”, SAT 2020 - 23^rd International Conference on Theory and Applications of Satisfiability Testing, vol. 12178, Lecture Notes in Computer Science, Alghero / Virtual, Italy, pp. 11-27 (2020)
  • V. Vallade, L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “On the Usefulness of Clause Strengthening in Parallel SAT Solving”, NFM 2020 - 12^th NASA Formal Methods Symposium, Moffett Field / Virtual, United States (2020)