Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information

This paper considers bounded model checking for extended labeled transition systems. Bounded model checking relies on a SAT solver to prove (or disprove) the existence of a counterexample with a bounded length. During the translation of a BMC problem to a SAT problem, much useful information is lost. This paper proposes an algorithm to analyze the transition system model, and then utilize the structure information hidden in the model to refine the decision ordering of variables in SAT solving. The basic idea is to guide the search process of SAT solving by the structure of the transition system. Experiments with this heuristic on real industrial designs show 5-12 times speedup over standard bounded model checking.