Efficient SAT Solving:  Beyond Supercubes

Domagoj Babic, Jesse Bingham, and Alan J. Hu

42nd ACM/IEEE Design Automation Conference (DAC),
ACM Press, 2005, pp. 744-749.


SAT (Boolean satisfiability) has become the primary Boolean reasoning
engine for many EDA applications, so the efficiency of SAT solving is
of great practical importance.  Recently, Goldberg \textit{et al.}
introduced \textit{supercubing}, a different approach to search-space
pruning, based on a theory that unifies many existing methods. Their
implementation reduced the number of decisions, but no speedup was
obtained. In this paper, we generalize beyond supercubes, creating a
theory we call \emph{B-cubing}, and show how to implement B-cubing in a
practical solver. On extensive benchmark runs, using both real problems
and synthetic benchmarks, the new technique is competitive on average
with the newest version of ZChaff, is much faster in some cases, and is
more robust.