Browse wiki
From International Center for Computational Logic
Modern propositional satisfiability (or SA … 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.ly used solving techniques can be modeled. +
@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}
}
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}
}
Hölldobler +
Steffen +
Steffen Hölldobler, Norbert Manthey, Tobia … Steffen Hölldobler, Norbert Manthey, Tobias Philipp, Peter Steinke<br/> '''[[WVPub6|<b>Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers</b>]]''' <br/>__NOTOC__In Daniel Le Berre, eds., <i>POS-14</i>, volume 27 of EPiC Series, 89-102, 2014. EasyChair<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[WVPub6|Details]]s]] +
Steffen Hölldobler, Norbert Manthey, Tobia … Steffen Hölldobler, Norbert Manthey, Tobias Philipp, Peter Steinke<br/> '''[[WVPub6/en|<b>Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers</b>]]''' <br/>__NOTOC__In Daniel Le Berre, eds., <i>POS-14</i>, volume 27 of EPiC Series, 89-102, 2014. EasyChair<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[WVPub6|Details]]s]] +
Display title of"Display title of" is a predefined property that can assign a distinct display title to an entity and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +
Modification date"Zuletzt geändert <span style="font-size:small;">(Modification date)</span>" is a predefined property that corresponds to the date of the last modification of a subject and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
11. Juni 2015, 12:27:41 +
Has query"Hat Abfrage <span style="font-size:small;">(Has query)</span>" is a predefined property that represents meta information (in form of a <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">subobject</a>) about individual queries and is provided by <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a>.
Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +, Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers + and Generic CDCL – A Formalization of Modern Propositional Satisfiability Solvers +
