Efficient SAT Solving: Beyond Supercubes
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@inproceedings{babic-bingham-hu-dac05,
author = {Domagoj Babi\'c and Jesse Bingham and Alan J.~Hu},
title = {{Efficient SAT Solving: Beyond Supercubes}},
booktitle = {DAC'05: Proceedings of the 42nd annual conference on
Design automation},
year = {2005},
pages = {744--749},
publisher = {ACM},
address = {New York, NY, USA},
location = {Anaheim, California, USA},
isbn = {1-59593-058-2},
doi = {http://doi.acm.org/10.1145/1065579.1065774},
}
Abstract:
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 et al.
introduced 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 B-cubing, and show how to implement Bcubing
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.