B-cubing: New possibilities for efficient SAT-solving
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.
sat boolean satisfiability search space pruning