Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/s13218-010-0008-4 | KI |
Keywords | Field | DocType |
sat solver,satisfiability,boolean circuits | Boolean circuit,Computer science,Boolean satisfiability problem,Satisfiability,Sequent calculus,Theoretical computer science,Conjunctive normal form,DPLL algorithm,Solver,Electronic circuit | Journal |
Volume | Issue | ISSN |
24 | 1 | 1610-1987 |
Citations | PageRank | References |
1 | 0.36 | 22 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Uwe Egly | 1 | 544 | 45.57 |
| Leopold Haller | 2 | 127 | 6.93 |