On the Usefulness of Clause Strengthening in Parallel SAT Solving

From LRDE

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