A SAT Solver for Circuits Based on the Tableau Method
| dc.contributor.author | Egly, Uwe | |
| dc.contributor.author | Haller, Leopold | |
| dc.date.accessioned | 2018-01-08T09:14:11Z | |
| dc.date.available | 2018-01-08T09:14:11Z | |
| dc.date.issued | 2010 | |
| dc.description.abstract | 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. | |
| dc.identifier.pissn | 1610-1987 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/11121 | |
| dc.publisher | Springer | |
| dc.relation.ispartof | KI - Künstliche Intelligenz: Vol. 24, No. 1 | |
| dc.relation.ispartofseries | KI - Künstliche Intelligenz | |
| dc.title | A SAT Solver for Circuits Based on the Tableau Method | |
| dc.type | Text/Journal Article | |
| gi.citation.endPage | 23 | |
| gi.citation.startPage | 15 |