B-Cubing: New Possibilities for Efficient SAT-Solving

[PDF] [PS] [PS.BZ2] [VIEW]

@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.