B-Cubing Theory: New Possibilities for Efficient SAT-Solving Domagoj Babic, Jesse Bingham, and Alan J. Hu 10th IEEE International Workshop on High-Level Design Validation and Test (HLDVT) IEEE Computer Society Press, 2005, pp. 192-199. 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.