Zeitschriftenartikel
A SAT Solver for Circuits Based on the Tableau Method
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Text/Journal Article
Zusatzinformation
Datum
2010
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Springer
Zusammenfassung
We present an extension of the BC tableau, a calculus for determining satisfiability of constrained Boolean circuits. We argue that a satisfiability decision procedure based on the BC tableau can be implemented as a non-clausal DPLL procedure and that therefore, advances to the DPLL framework can be integrated into such a tableau procedure. We present a prototypical implementation of these ideas and evaluate it using a set of benchmark instances. We show that the extensions increase the efficiency of the basic BC tableau considerably and compare the performance of our solver with that of the non-clausal solver NoClause and the CNF-based SAT solver MiniSat.