evaluates to 0 if either f1 or f2 evaluate
to 0
f ˲
1 ∨ f2 is a formula that evaluates to
0 when f1 and f2 both evaluate to 0, and
evaluates to 1 if either f1 or f2 evaluate
to 1
IllustratIon by GWen Vanhee
(x1 ∨ Øx2) ∧ x3 is an example formula
constructed using these rules. Given a
valuation of the variables, these rules
can be used to determine the valuation
of the formula. For example: when (x1
= 0, x2 = 0, x3 = 1), this formula evaluates to 1 and when (x3 = 0), this formula
evaluates to 0, regardless of the values
of x1 and x2. This example also illustrates how the operators in the formula
provide constraints on the variables.
In this example, for this formula to be
true (evaluate to 1), x3 must be 1.
Boolean satisfiability
A satisfying assignment for a formula
is an assignment of the variables such
that the formula evaluates to 1. It simultaneously satisfies the constraints
imposed by all the operators in the
formula. Such an assignment may not
always exist. For example the formula (Øx1 ∨ Øx2) ∧ (x1 ∨ x2) ∧ (Øx1 ∨ x2) ∧
(x1 ∨ Øx2) cannot be satisfied by any
of the four possible assignments 0/0,
0/1, 1/0, 1/1 to x1 and x2. In this case
the problem is overconstrained. This
leads us to a definition of the Boolean
Satisfiability problem (also referred to
as Propositional Satisfiability or just
Satisfiability, and abbreviated as SAT):
Given a formula, find a satisfying assignment or prove that none exists. This is the
constructive version of the problem,
and one used in practice. A simpler decision version, often used on the theoretical side, just needs to determine if
there exists a satisfying assignment for
the formula (a yes/no answer). It is easy
to see that a solver for the decision version of the problem can easily be used
to construct a solution to the constructive version, by solving a series of n decision problems where n is the number
of variables in a formula.
Many constraint satisfaction problems dealing with non-Boolean variables can be relatively easily translated
to SAT. For example, consider an instance of the classic graph coloring
problem where an n-vertex graph needs
to be checked for 4-colorability, that is,
determining whether each vertex can
be colored using one of four possible
colors such that no two adjacent vertices have the same color. In this case,
the variables are the colors {c0, c1, c2,
…, cn– 1} for the n vertices, and the constraints are that adjacent vertices must
have different colors. For this problem
the variables are not Boolean and the
constraints are not directly expressed
with the operators {∧, ∨, Ø}. However,
the variables and constraints can be
encoded into a propositional formula
as follows. Two Boolean variables, ci0,
ci1, are used in a two-bit encoding of
the four possible values of the color for
vertex i. Let i and j be adjacent vertices.