Name
Abstract | ||
|---|---|---|
SAT (Boolean satisfiability) has become the primary Boolean reasoning engine for many EDA (electronic design automation) applications, so the efficiency of SAT-solving is of great practical importance. B-cubing is our extension and generalization of Goldberg et al.'s supercubing, an approach to pruning in SAT-solving completely different from the standard approach used in leading solvers. We have built a B-cubing-based solver that is competitive with, and often outperforms, leading conventional solvers (e.g., ZChaff II) on a wide range of EDA benchmarks. However, B-cubing is hard to understand and even the correctness of the algorithm is not obvious. This paper presents the theoretical basis for B-cubing, proves our approach correct, details our implementation and experimental results, and maps out other correct possibilities for further improving SAT-solving. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/TC.2006.175 | IEEE Trans. Computers |
Keywords | Field | DocType |
boolean algebra,boolean satisfiability,electronic design automation,computability,sat | Maximum satisfiability problem,#SAT,Boolean circuit,Computer science,Boolean satisfiability problem,Theoretical computer science,Standard Boolean model,And-inverter graph,Circuit minimization for Boolean functions,Boolean expression | Journal |
Volume | Issue | ISSN |
55 | 11 | 0018-9340 |
Citations | PageRank | References |
5 | 0.41 | 22 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Domagoj Babic | 1 | 192 | 10.51 |
| Jesse D. Bingham | 2 | 10 | 1.22 |
| Alan J. Hu | 3 | 1427 | 148.29 |