Abstract
In this article1, we present a small, complete, and efficient SAT-solver in the style of conflict-driven learning, as exemplified by CHAFF. We aim to give sufficient details about implementation to enable the reader to construct his or her own solver in a very short time. This will allow users of SAT-solvers to make domain specific extensions or adaptions of current state-of-the-art SAT-techniques, to meet the needs of a particular application area. The presented solver is designed with this in mind, and includes among other things a mechanism for adding arbitrary boolean constraints. It also supports solving a series of related SAT-problems efficiently by an incremental SAT-interface. © Springer-Verlag 2004.
Cite
CITATION STYLE
Eén, N., & Sörensson, N. (2004). An extensible SAT-solver. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2919, 502–518. https://doi.org/10.1007/978-3-540-24605-3_37
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
