proposed over the years. In particular, a technique called conflict-driven
learning and non-chronological backtracking2, 24 has greatly enhanced the
power of DPLL SAT solvers on problem
instances arising from real applications, and has become a key element of
modern SAT solvers. The technique is
illustrated in Figure 3. The column on
the left lists the clauses in the example
formula. The colors of the literals show
the current assignments during the
search (red representing 0, green 1,
and black representing unassigned).
The middle graph shows the branching and implications at the current
point in the search. At each vertex the
branching assignment is shown in blue
and the implications in gray. The first
branching is on x1, and it implies x4= 1
(because of the first clause), the second
branching is on x3, and it implies x8=0
and x12= 1 and so on. The right graph
shows the implication relationships
between variables. For example, x4= 1
is implied because of x1=0, so there is
a directed edge from node x1=0 to node
x4= 1. x8=0 is implied because of both
x1=0 and x3= 1 (the red literals in the
second clause), therefore, these nodes
have edges leading to x8=0.
After branching on x7 and implying
x9= 1 because of the 5th clause, we find
that the 6th clause becomes a conflicting clause and the solver has to backtrack. Instead of flipping the last decision variable x7 and trying x7=0, we can
learn some information from the conflict. From the implication graph, we
see that there is a conflict because x9 is
implied to be both 1 and 0. If we consider a cut (shown as the orange line)
separating the conflicting implications from the branching decisions, we
know that once the assignments corresponding to the cut edges are made,
we will end up with a conflict, since no
further decisions are made. Thus, the
edges that cross the cut are, in some
sense, responsible for the conflict. In
the example, x3, x7, and x8 have edges
cross the cut, thus the combination of
x3= 1, x7= 1, and x8=0 results in the conflict. We can learn from this and ensure
that this assignment combination is
not tried in the future. This is accomplished by recording the condition (Øx3
∨ Øx7 ∨ x8). This clause, referred to as
a learned clause, can be added to the
formula. While it is redundant in the
sense that it is implied by the formula,
it is nonetheless useful as it prevents
search from ever making the assignment (x3= 1, x7= 1, x8=0) again.
Further, because of this learned
clause, x7 = 1 is now implied after the
second decision, and we can backtrack
to this earlier decision level as the
choice of x2 = 0 is irrelevant to the current conflict. Since such backtracking
skips branches, it is called non-chronological backtracking and helps prune
away unsatisfiable parts of the search
space.
Recent Results
Recent work has exposed several significant areas of improvement now integral to modern SAT solvers.
22 The first
deals with efficient implementation of
figure 4. speedup of sAT solvers in recent years.
Relative solving time (log scale)
1000
>500
100
10
33. 5
6. 8
4
4. 3
1. 7
1
Grasp (2000)
zchaff(2001)
Berkmin (2002–03)
zchaff (2003–04)
siege (2004)
1. 2
minisat + satelite
(2005)
minisat2 (2006)
1
Rsat + satelite
(2007)
solver
the unit-clause rule using a technique
called two-literal watching. The second
area relates to improvements in the
branching step by focusing on exhausting local sub-spaces before moving to
new spaces. This is accomplished by
placing increased emphasis on variables present in recently added conflict clauses. Another commonly used
technique is random restart,
13 which
periodically restarts the search while
retaining the learned clauses from the
current search to avoid being stuck in
a search sub-space for too long. Other
recent directions include formula
preprocessing for clause and variable
elimination,
11 considering algorithm
portfolios that use empirical hardness
models to choose among their constituent solvers on a per-instance basis39 and using learning techniques to
adjust parameters of heuristics.
16 With
the advent of multicore processing,
there is emerging interest in efficient
multi-core implementations of parallel SAT solvers.
14
The original Davis Putnam algorithm10 based on resolution is often
regarded as the first algorithm for SAT
and has great theoretical and historical
significance. However, this algorithm
suffers from a space growth problem
that makes it impractical. Reduced Ordered Binary Decision Diagrams (
ROBDDs)
5 are a canonical representation of
logic functions, that is, each function
has a unique representation for a fixed
variable ordering. Thus, ROBDDS can
be used directly for SAT. However, ROBDDs also face space limitations with
increasing instance size. Stålmarck’s
algorithm35 uses breadth-first search
instead of depth-first search as in
DPLL, and has been shown to be practically useful. Its performance relative to
DPLL based solvers is unclear as public
versions of efficient implementations
of Stålmarck’s algorithm are not available due to its proprietary nature.
When represented in CNF, SAT can
be regarded as a discrete optimization
problem with the objective to maximize
the number of satisfied clauses. If this
max value is equal to the total number
of clauses, then the instance is satisfiable. Many discrete optimization techniques have been explored in the SAT
context, including simulated annealing,
33 tabu search,
25 neural networks,
34
and genetic algorithms.
23