Sciweavers

Share
DAC
2004
ACM

Refining the SAT decision ordering for bounded model checking

11 years 3 months ago
Refining the SAT decision ordering for bounded model checking
Bounded Model Checking (BMC) relies on solving a sequence of highly correlated Boolean satisfiability (SAT) problems, each of which corresponds to the existence of counter-examples of a bounded length. These satisfiability problems are usually decided by SAT solvers, whose performance depends heavily on the variable decision ordering. The satisfiability problems in BMC have some unique characteristics that can be used to help the SAT decision making, but so far they have not been explored by the decision heuristics of most modern SAT solvers. We propose an algorithm to exploit the correlation among the sequence of SAT problems in BMC, by predicting and successively refining a partial variable ordering. This variable ordering is computed based on the analysis of all previous unsatisfiable instances, and is then combined with the SAT solver's existing decision heuristic to determine the final variable decision ordering. Experiments on real designs from industry showed that our new ...
Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio So
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2004
Where DAC
Authors Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi
Comments (0)
books