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.

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