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