A variation of the optimization approach, first proposed in the early 1990s, solves SAT using local search (for example, GSAT31). The algorithm first randomly selects a value for each variable, and calculates how many clauses are satisfied. If not all clauses are satisfied, it repeatedly flips the value of a variable to increase the number of the clauses satisfied. If no such variable is available, it accepts a decrease in the objective function by either flipping a random variable, or restarting from a fresh set of variable assignments. This is accelerated further, by confining the flips to literals in clauses not satisfied by the current assignment. 30 This simple algorithm, when carefully implemented, is surprisingly effective on certain classes of SAT instances. Unfortunately, this algorithm is incomplete in the sense that while it may be able to find an assignment for a satisfiable SAT instance, it cannot prove an instance to be unsatisfiable. More recently, incomplete solvers based on a technique called survey propagation4 have been found to be very effective for certain classes of SAT instances and have attracted much attention in the theory community.

 

The Role of Benchmarks It is important to note the role of practical benchmarks in the development of modern SAT solvers. These benchmarks are critical in tuning the solvers to various classes of practical instances (that is, instances generated from real-world applications). While we do not have deep insight into how these solvers exploit the special structure found in these instances, we do know that the structure is critical in our ability to tackle them. (There exists some recent work that provides initial insights into the effect of structure on DPLL search. 37, 38) Experimental research in SAT solvers has been enabled in large part by benchmarks put forward collectively by the research community, and the challenge in the form of a SAT solver competition that is held regularly with the International Conference on Theory and Applications of Satisfiability Testing (SAT).b The community has also benefited from the SATLive portal, which has provided widespread

 

b http://www.satcompetition.org/.

one of the more
prominent practical
applications of
sAT has been in
the design and
verification of
digital circuits.
The functionality
of digital circuits
can be expressed
as compositions of
basic logic gates.

dissemination of links to SAT articles and software.c

Figure 4 provides some data on the improvements in SAT solvers at the SAT Competition in recent years.d It plots the relative solving times for a set of solvers developed over the last 10 years. This includes solvers that placed first in the industrial benchmarks category of the SAT competitions. The solvers were run on a set of benchmarks from hardware and software verification (not used in the competitions). 32 This is normalized to the best solver in the 2007 competition (RSAT with the SatElite preprocessor). The slow-down of the Grasp solver is a lower bound, since it could not complete some of the benchmarks in the 10,000-second time limit. While this study is limited to a specific set of benchmarks, it is indicative of the progress in SAT solvers since 2000.

Industrial Impact

SAT solvers are maturing to the point that developers are using them in a range of application domains, much like mathematical programming tools or linear equation solvers. Early use of SAT was seen in planning in artificial intelligence with practical use in space exploration. 27 Recent increases in the capacity of commercial solvers has enabled widespread use in the electronic design automation (EDA) industry as the reasoning engine behind verification and testing tools such as automatic test pattern generators, 21 equivalence checkers, and property checkers. SAT-based bounded model checkers have been used in industrial microprocessor verification. 7 More recently, SAT has also been used in tools for software verification and debugging, for example, industrial verification of device drivers using SAT-based model checking,e as well as SAT-based static analysis.f Outside of verification and testing, SAT techniques have also been applied in configuration management such as resolving software package dependencies.g

 

c http://www.satlive.org/.
d Provided by Sanjit Seshia, UC Berkeley.
e http://www.microsoft.com/whdc/DevTools/
tools/ SDV.mspx.
f http://www.coverity.com/index.html.
g http://news.opensuse.org/2008/06/06/sneak-
peeks-at-opensuse-110-package-manage-
ment-with-duncan-mac-vicar/.