Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers

Steffen HölldoblerSteffen Hölldobler, Norbert MantheyNorbert Manthey, Tobias PhilippTobias Philipp, Peter SteinkePeter Steinke

Steffen Hölldobler, Norbert Manthey, Tobias Philipp, Peter Steinke
Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers
In Daniel Le Berre, eds., POS-14, volume 27 of EPiC Series, 89-102, 2014. EasyChair

Details
Bibtex

KurzfassungAbstract
Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial. In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

@inproceedings{HMPS2014,
  author    = {Steffen H{\"{o}}lldobler and Norbert Manthey and Tobias Philipp
               and Peter Steinke},
  title     = {Generic {CDCL} {\textendash} A Formalization of Modern
               Propositional Satisfiability Solvers},
  editor    = {Daniel Le Berre},
  booktitle = {POS-14},
  series    = {EPiC Series},
  volume    = {27},
  publisher = {EasyChair},
  year      = {2014},
  pages     = {89-102}
}