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