LE FRIOUX Ludovic
责任导师 : Fabrice KORDON
助理责任导师 : BAARIR Souheib, KORDON Fabrice, SOPENA Julien
Towards more efficient parallel SAT solving
Boolean SATisfiability has been used successfully in many applicative contexts.
This is due to the capability of modern SAT solvers to solve complex problems
involving millions of variables. Most SAT solvers have long been sequential and
based on the CDCL algorithm. The emergence of many-core machines opens new
possibilities in this domain.
There are numerous parallel SAT solvers that differ by their strategies,
programming languages, etc. Hence, comparing the efficiency of the theoretical
approaches in a fair way is a challenging task. Moreover, the introduction of a
new approach needs a deep understanding of the existing solvers'
implementations.
We present Painless: a framework to build parallel SAT solvers for many-core
environments. Thanks to its genericness and modularity, it provides the
implementation of basics for parallel SAT solving. It also enables users to
easily create their parallel solvers based on new strategies.
Painless allowed to build and test existing strategies by using different
chunk of solutions present in the literature. We were able to easily mimic the
behaviour of three state-of-the-art solvers by factorising many parts of their
implementations. The efficiency of Painless was highlighted as these
implementations are at least efficient as the original ones. Moreover, one of
our solvers won the SAT Competition'18.
Going further, Painless enabled to conduct fair experiments in the context of
divide-and-conquer solvers, and allowed us to highlight original compositions of
strategies performing better than already known ones. Also, we were able to
create and test new original strategies exploiting the modular structure of SAT
instances.
答辩 : 2019-7-3
评委会 :
Michaël KRAJECKI, Professeur à l'Université de Reims, CReSTIC [Rapporteur]
Laurent SIMON, Professeur à l'Université de Bordeaux, LaBRI, CNRS [Rapporteur]
Daniel LE BERRE, Professeur à l'Université d'Artois, CRIL, CNRS
Bertrand LE CUN, Ingénieur Senior à Google Inc.
Clémence MAGNIEN, Directeur de Recherche au CNRS, LIP6, CNRS
Souheib BAARIR, Maître de Conférence à l'Université Paris Nanterre, LIP6, CNRS
Fabrice KORDON, Professeur à Sorbonne Université, LIP6, CNRS
Julien SOPENA, Maître de Conférence à Sorbonne Université, LIP6, CNRS, INRIA
2017-2020 刊物
-
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 - 23rd 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 - 12th NASA Formal Methods Symposium, Moffett Field / Virtual, United States (2020)
-
2019
- L. Le Frioux : “Vers une parallélisation efficace de la résolution du problème de satisfaisabilité”, 博士论文, 答辩 2019-7-3, 责任导师 Kordon, Fabrice, 助理责任导师 : Baarir, Souheib, Kordon, Fabrice, Sopena, Julien (2019)
- L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework”, TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 11427, Lecture Notes in Computer Science, Prague, Czechia, pp. 135-151 (2019)
-
2017
- L. Le Frioux, S. Baarir, J. Sopena, F. Kordon : “PaInleSS: a Framework for Parallel SAT Solving”, The 20th International Conference on Theory and Applications of Satisfiability Testing, vol. 10491, Lecture Notes in Computer Science, Melbourne, Australia, pp. 233-250, (Springer) (2017)