DocumentCode :
3620636
Title :
B-cubing theory: new possibilities for efficient SAT-solving
Author :
D. Babic;J. Bingham;A.J. Hu
Author_Institution :
Dept. of Comput. Sci., British Columbia Univ., Vancouver, BC, Canada
fYear :
2005
fDate :
6/27/1905 12:00:00 AM
Firstpage :
192
Lastpage :
199
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.
Keywords :
"Electronic design automation and methodology","Engines","Computer science","Application software","Field programmable gate arrays","Routing","Automatic test pattern generation","Electronic equipment testing","Automatic testing"
Publisher :
ieee
Conference_Titel :
High-Level Design Validation and Test Workshop, 2005. Tenth IEEE International
ISSN :
1552-6674
Print_ISBN :
0-7803-9571-9
Type :
conf
DOI :
10.1109/HLDVT.2005.1568836
Filename :
1568836
Link To Document :
بازگشت