B-Cubing Theory: New Possibilities for Efficient SAT-Solving

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

@inproceedings{babic-bingham-hu-hldvt2005,
  author = {Domagoj Babi\'c and Jesse Bingham and Alan J. Hu},
  title = {{B-Cubing Theory: New Possibilities for Efficient SAT-Solving}},
  booktitle = {HLDVT'05: Proceedings of the 10th International High-Level 
    Design Validation and Test Workshop},
  year = {2005},
  publisher = {IEEE Computer Society},
  address = {Washington, DC, USA},
  pages = {192--199},
  isbn = {0-7803-9571-9},
  doi = {http://dx.doi.org/10.1109/HLDVT.2005.1568836},
}

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 clarifies the theoretical basis for B-cubing, proves our approach correct, and maps out other correct possibilities for further improving SAT-solving.