Painless
From LRDE
Revision as of 11:15, 30 January 2020 by Ludovic Le Frioux (talk | contribs)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
PArallel INstantiabLE Sat Solver (Painless) is a framework written in C++ that simplifies the implementation and evaluation of new parallel SAT solvers for many-core environments. The components of Painless can be instantiated independently to produce a new complete solver. The guiding principle is to separate the technical components dedicated to some specific aspect of concurrent programming, from the components implementing heuristics and optimizations embedded in a parallel SAT solver.
Painless has been developed by the LRDE, the MoVe team at LIP6, and the DELYS team at LIP6 / Inria.
Source Code (GPLv3)
Awards
Painless-MapleCOMSPS won 1st in the SAT Competition 2018 parallel track!
- See solver description for details.
- Source code is available here.
Painless-MapleCOMSPS won 3rd in the SAT Competition 2017 parallel track!
- See solver description for details.
- Source code is available here.
Related Publications
- Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework in Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19)
- painless-mcomsps and painless-mcomsps-sym in Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions
- Painless: a Framework for Parallel SAT Solving in Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17)
- painless-maplecomsps in Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions