An extensible SAT-solver. (English) Zbl 1204.68191

Eén, Niklas; Sörensson, Niklas

Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 502-518 (2004).

Summary: In this article (extended version available at http://www.cs.chalmers.se/~een), 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 adaptations 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.
For the entire collection see [Zbl 1030.00034].

MSC:

68T20

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Chaff; MiniSat; SATIRE