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