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 Steffen Hölldobler and Andrey Malikov and Christoph Wernhard, eds., Proceedings of the Young Scientists' International Workshop on Trends in Information Processing, 2014

Details
Bibtex

KurzfassungAbstract
Abstract. 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. 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 adequately modeled. Finally, we compare Generic CDCL with related systems.
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    = {Steffen H{\"{o}}lldobler and Andrey Malikov and Christoph
               Wernhard},
  booktitle = {Proceedings of the Young Scientists' International Workshop on
               Trends in Information Processing},
  year      = {2014}
}