Logo des Repositoriums
 
Zeitschriftenartikel

A SAT Solver for Circuits Based on the Tableau Method

Vorschaubild nicht verfügbar

Volltext URI

Dokumententyp

Text/Journal Article

Zusatzinformation

Datum

2010

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.

Beschreibung

Egly, Uwe; Haller, Leopold (2010): A SAT Solver for Circuits Based on the Tableau Method. KI - Künstliche Intelligenz: Vol. 24, No. 1. Springer. PISSN: 1610-1987. pp. 15-23

Schlagwörter

Zitierform

DOI

Tags