review articles
DoI: 10.1145/1536616.1536637
Satisfiability solvers can now be effectively
deployed in practical applications.
BY shARAD mALIK AnD LIn TAo zhAnG
Boolean
satisfiability
from Theoretical
hardness to
Practical success
tHeRe ARe mAny practical situations where we need
to satisfy several potentially conflicting constraints.
simple examples of this abound in daily life, for
example, determining a schedule for a series of games
that resolves the availability of players and venues, or
finding a seating assignment at dinner consistent with
various rules the host would like to impose. This also
applies to applications in computing, for example,
ensuring that a hardware/software system functions
correctly with its overall behavior constrained by the
behavior of its components and their composition,
or finding a plan for a robot to reach a goal that is
consistent with the moves it can make at any step.
While the applications may seem varied, at the
core they all have variables whose values we need to
determine (for example, the person sitting at a given
seat at dinner) and constraints that these variables
must satisfy (for example, the host’s seating rules).
In its simplest form, the variables
are Boolean valued (true/false, often
represented using 1/0) and
propositional logic formulas can be used to express
the constraints on the variables.
15 In
propositional logic the operators AND,
OR, and NOT (represented by the symbols ∧, ∨, and Ø respectively) are used
to construct formulas with variables.
If x is a Boolean variable and f, f1 and
f2 are propositional logic formulas
(subsequently referred to simply as
formulas), then the following recursive
definition describes how complex formulas are constructed and evaluated
using the constants 0 and 1, the variables, and these operators.
x ˲ is a formula that evaluates to 1
when x is 1, and evaluates to 0 when x
is 0
Ø ˲ f is a formula that evaluates to 1
when f evaluates to 0, and 0 when f
evaluates to 1
f ˲
1 ∧ f2 is a formula that evaluates to
1 when f1 and f2 both evaluate to 1, and
