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