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.