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 ...

• Type: Conference
• Year: 2004
• Where: DAC
• Authors: Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio Somenzi
• Keywords: DAC 2004, Design Automation, Final Variable Decision, Modern Sat Solvers, SAT Decision