I am happy to announce that the following paper has been
accepted at the 20th International Conference on Theory and Applications of Satisfiability Testing to be held in
Melbourne, Australia from August 28th to September 1st.
"PaInleSS: a Framework for Parallel SAT Solving"
Ludovic Le Frioux (1,2), Souheib Baarir (1,2,3), Julien Sopena (2), and Fabrice Kordon (2)
(1) LRDE, EPITA, Kremlin-Bicêtre, France
(2) Sorbonne Universites, UPMC Univ Paris 06, UMR 7606, LIP6, Paris, France CNRS, UMR 7606, LIP6, Paris, France
(3) Universite Paris Nanterre, France.
Abstract :
Over the last decade, parallel SAT solving has been widely
studied from both theoretical and practical aspects. There are now numerous
solvers that dier by parallelization strategies, programming languages,
concurrent programming, involved libraries, etc.
Hence, comparing the eciency of the theoretical approaches is a challenging
task. Moreover, the introduction of a new approach needs either
a deep understanding of the existing solvers, or to start from scratch the
implementation of a new tool.
We present PaInleSS: a framework to build parallel SAT solvers for
many-core environments. Thanks to its genericity and modularity, it provides
the implementation of basics for parallel SAT solving like clause
exchanges, Portfolio and Divide-and-Conquer strategies. It also enables
users to easily create their own parallel solvers based on new strategies.
Our experiments show that our framework compares well with some of
the best state-of-the-art solvers.
Souheib Baarir.
