figure 1. encoding of graph coloring.

1

Ø(((c10 ∧ c20) ∨ (Øc10 ∧ Øc20)) ∧ ((c11 ∧ c21) ∨ (Øc11 ∧ Øc21))) ∧ Ø(((c10 ∧ c30) ∨ (Øc10 ∧ Øc30)) ∧ ((c11 ∧ c31) ∨ (Øc11 ∧ Øc31))) ∧ Ø(((c30 ∧ c20) ∨ (Øc30 ∧ Øc20)) ∧ ((c31 ∧ c21) ∨ (Øc31 ∧ Øc21))) encoding

c10 = 0 ∧ c11 = 0 ∧ c20 = 0 ∧ c21 = 1 ∧ c30 = 1 ∧ c31 = 0

solution

2

3

 

The constraint ci ≠ cj is then expressed as Ø((ci0 == cj0) ∧ (ci1 == cj1)), here == represents equality and thus this condition checks that both bits in the encoding do not have the same value for i and j. Further, (ci0 == cj0) can be expressed as (ci0 ∧ cj0) ∨ (Øci0 ∧ Øcj0), that is, they are both 1 or both 0. Similarly for (ci1 == cj1). If we take the conjunction of the constraints on each edge, then the resulting formula is satisfiable if and only if the original graph coloring problem has a solution. Figure 1 illustrates an instance of the encoding of the graph coloring problem into a Boolean formula and its satisfying solution.

Encodings have been useful in translating problems from a wide range of domains to SAT, for example, scheduling basketball games, 40 planning in artificial intelligence, 20 validating software models, 17 routing field programmable gate arrays, 28 and synthesizing consistent network configurations. 29 This makes SAT solvers powerful engines for solving constraint satisfaction problems. However, SAT solvers are not always the best engines—there are many cases where specialized techniques work better for various constraint problems, including graph coloring (for example, Johnson et al. 19). Nonetheless, it is often much easier and more efficient to use off-the-shelf SAT solvers than developing specialized tools from scratch.

One of the more prominent practical applications of SAT has been in the design and verification of digital circuits. Here, the translation to a formula is very straightforward. The functionality of digital circuits can be expressed as compositions of basic logic gates. A logic gate has Boolean input signals and produces Boolean output signals. The output of a gate can be used as an input to another gate. The functions of

the basic logic gates are in direct correspondence to the operators {∧, ∨, Ø}. Thus various properties regarding the functionality of logic circuits can be easily translated to formulas. For example, checking that the values of two signals s1 and s2 in the logic circuit are always the same is equivalent to checking that their corresponding formulas f1 and f2 never differ, that is, (f1 ∧ Øf2) ∨ (Øf1 ∧ f2) is not satisfiable.

This technique can be extended to handle more complex properties involving values on sequences of signals, for example, a request is eventually acknowledged. For such problems, techniques that deal with temporal properties of the system, such as model checking, are used. 6 Modern SAT solvers have also been successfully applied for such tasks. 3, 26 One of the main difficulties of applying SAT in checking such properties is to find a way to express the concept of “eventually.” In theory, there is no tractable way to express this using propositional logic. However, in practice it is often good enough to just set a bound on the number of steps. For example, instead of asking whether a response to a request will eventually occur, we ask whether there will be a response within k clock cycles, where k is a small fixed number. Similar techniques have also been used in AI planning, 20 for example, instead of determining if a goal is reachable, we ask whether we can reach the goal in k steps. This unrolling technique has been widely adopted in practice, since we often only care about the behavior of the system within a small bounded number of steps.

isfying solution, belongs to the class of problems known as NP-complete. 8, 12 An instance of any one of these problems can be relatively easily transformed into an instance of another. For example, both graph coloring and SAT are NP-complete, and earlier we described how to transform a graph coloring instance to a SAT instance.

All currently known solutions for NP-Complete problems, in the worst case, require runtime that grows exponentially with the size of the instance. Whether there exist subexponential solutions to NP-Complete problems is arguably the most famous open question in computer science.a Although there is no definitive conclusion, the answer is widely believed to be in the negative. This exponential growth in time complexity indicates the difficulty of scaling solutions to larger instances.

However, an important part of this characterization is “worst case.” This holds out some hope for the “typical case,” and more importantly the typical case that might arise in specific problem domains. In fact, it is exactly the non-adversarial nature of practical instances that is exploited by SAT solvers.

solving sAT

Most SAT solvers work with a restricted representation of formulas in conjunctive normal form (CNF), defined as follows. A literal l is either a positive or a negative occurrence of a variable (for example, x or Øx). A clause, c, is the OR of a set of literals, such as (l1 ∨ l2 ∨ l3 … ∨ ln). A CNF formula is the AND of a set of clauses, such as (c1 ∧ c2 ∧ c3 ∧ cm). An example CNF formula is:

 

(Øx1 ∨ Øx2) ∧ (Øx1 ∨ x2 ∨ Øx3) ∧ (Øx1 ∨ x3 ∨ Øx4) ∧ (x1 ∨ x4)

 

Theoretical hardness: sAT and nP-completeness The decision version of SAT, that is, determining if a given formula has a sat-

The restriction to CNF is an active choice made by SAT solvers as it enables their underlying algorithms. Further, this is not a limitation in terms of the formulas that can be handled. Indeed, with the addition of new auxiliary variables; it is easy to translate any formula into CNF with only a linear increase in size. 36 However, this representation is not used exclusively and there has been recent success with