IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Ofer Shtrichman

Weizmann Institute


Some Experiments with Variable Orderings, in the Context of SAT-based Bounded Model Checking

The use of SAT methods for Symbolic Model Checking, rather than the more traditional Binary Decision Diagrams (BDDs) has recently been introduced in the framework of Bounded Model Checking (BMC).
The basic idea is to search for a counter example in executions whose length are bounded by some integer $k$. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDD's.

The first experiments with this idea showed that if $k$ is small enough, or if the model has certain characteristics, it outperforms BDD-based techniques. While traditional SAT procedures are designed for efficient solving of any propositional formula, the unique characteristics of BMC formulas can be exploited for optimizing them in various ways. In particular, it seems that fixing a variable order has a strong effect on the results (traditionally this order is computed dynamically).

We will show the impact of various ordering strategies, and speculate on the reasons for their relative success.
Some thoughts and directions for future research in this field will be presented as well.

(Note: most but not all topics in this talk were presented in the IBM HRL seminar in February 2000, and in CAV'2000, under the title "Tuning SAT Checkers for Bounded Model Checking". The main difference is the discussion on the various variable ordering strategies).