CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

An Extensible SAT-solver

Niklas Sörensson ; Niklas Een (Institutionen för datavetenskap)
Lecture Notes in Computer Science. 6th International Conference on Theory and Applications of Satisfiability Testing, Santa Margherita Ligure, Italy, 5-8 May 2003 (0302-9743). Vol. 2919 (2003), p. 502-518.
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2008-09-24. Senast ändrad 2013-03-13.
CPL Pubid: 74325


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)
Institutionen för datavetenskap (2002-2004)


Datavetenskap (datalogi)

Chalmers infrastruktur