On the Usefulness of Clause Strengthening in Parallel SAT Solving

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

• Paper

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.}
}