On the Usefulness of Clause Strengthening in Parallel SAT Solving
From LRDE
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.
- Authors
- Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Fabrice Kordon
- Where
- Proceedings of the 12th NASA Formal Methods Symposium (NFM'20)
- Type
- inproceedings
- Publisher
- Springer, Cham
- Keywords
- Parallel satisfiability, tool, strengthening, clause sharing, portfolio, divide-and-conquer
- Date
- 2020-08-01
Abstract
In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.
Documents
Bibtex (lrde.bib)
@InProceedings{ vallade.20.nfm, author = {Vincent Vallade and Ludovic {Le Frioux} and Souheib Baarir and Julien Sopena and Fabrice Kordon}, title = {On the Usefulness of Clause Strengthening in Parallel {SAT} Solving}, booktitle = {Proceedings of the 12th NASA Formal Methods Symposium (NFM'20)}, doi = {10.1007/978-3-030-55754-6_13}, year = 2020, month = aug, volume = {12229}, pages = {222--229}, series = {Lecture Notes in Computer Science}, publisher = {Springer, Cham}, abstract = {In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.} }