Tenth IEEE International High-Level Design Validation and Test Workshop, 2005.
Download PDF

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. (2002) 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.
Like what you’re reading?
Already a member?Sign In
Member Price
$11
Non-Member Price
$21
Add to CartSign In
Get this article FREE with a new membership!