B-Cubing: New Possibilities for Efficient SAT-Solving
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@article{bbh06bcubing,
author = {Domagoj Babi\'c and Jesse Bingham and Alan J.~Hu},
title = {{B-Cubing: New Possibilities for Efficient SAT-Solving}},
journal = {IEEE Trans. Computers},
volume = {55},
number = {11},
year = {2006},
pages = {1315--1324},
publisher = {IEEE Computer Society},
}
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.