N. Eén, and N. Sörensson. Theory and Applications of Satisfiability Testing, page 502--518. Berlin, Heidelberg, Springer Berlin Heidelberg, (2004)
Abstract
In this article, 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.
%0 Conference Paper
%1 10.1007/978-3-540-24605-3_37
%A Eén, Niklas
%A Sörensson, Niklas
%B Theory and Applications of Satisfiability Testing
%C Berlin, Heidelberg
%D 2004
%E Giunchiglia, Enrico
%E Tacchella, Armando
%I Springer Berlin Heidelberg
%K minisat sat sat_solver
%P 502--518
%T An Extensible SAT-solver
%X In this article, 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.
%@ 978-3-540-24605-3
@inproceedings{10.1007/978-3-540-24605-3_37,
abstract = {In this article, 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.},
added-at = {2019-06-05T13:46:26.000+0200},
address = {Berlin, Heidelberg},
author = {E{\'e}n, Niklas and S{\"o}rensson, Niklas},
biburl = {https://www.bibsonomy.org/bibtex/25fe48958890e631c7f0979018a2104c7/duerrschnabel},
booktitle = {Theory and Applications of Satisfiability Testing},
editor = {Giunchiglia, Enrico and Tacchella, Armando},
interhash = {9ea45cbd035ed178d38f2ff832bf35b2},
intrahash = {5fe48958890e631c7f0979018a2104c7},
isbn = {978-3-540-24605-3},
keywords = {minisat sat sat_solver},
pages = {502--518},
publisher = {Springer Berlin Heidelberg},
timestamp = {2019-06-05T13:46:26.000+0200},
title = {An Extensible SAT-solver},
year = 2004
}