### 4.6.1 Exploiting Propositional Structure

A fundamental idea in AI is to exploit structure in a domain. One form of structure for CSPs arises from the exploitation of aspects of restricted classes of variables
and constraints. One such class is the
class of **propositional
satisfiability**
problems. These problems are characterized
by

- Boolean variables: a Boolean
variable is a variable with domain
*{true,false}*. Given a Boolean variable*Happy*, the proposition*happy*means*Happy=true*, and*¬happy*means*Happy=false*. - clausal constraints: a
**clause**is an expression of the form*l*, where each_{1}∨ l_{2}∨ ...∨ l_{k}*l*is a literal. A_{i}**literal**is an assignment of a value to a Boolean variable. A clause is satisfied, or true, in a possible world if and only if at least one of the literals that makes up the clause is true in that possible world.

For
example, the clause *happy ∨ sad ∨ ¬living* is a constraint
among the variables *Happy*, *Sad*, and *Living*, which is true if
*Happy* has value *true*, *Sad* has value *true*, or *Living* has
value *false*.

A clause is a constraint on a set of Boolean variables that removes
one of the assignments from consideration - the assignment that makes
all literals false. Thus, the clause *happy ∨ sad ∨ ¬living* specifies that the assignment * ¬happy*,
* ¬sad*, *living* is not allowed.

When there are only two values, pruning a value from the domain is equivalent to
assigning the opposite value. Thus, if *X* has domain
*{true,false}*, pruning *true* from the domain of *X* is the same as assigning *X* to have
value *false*.

Arc consistency can be used to prune the set of values and the set of constraints. Assigning a value to a Boolean variable can simplify the set of constraints:

- If
*X*is assigned*true*, all of the clauses with*X=true*become redundant; they are automatically satisfied. These clauses can be removed. Similarly, assigning the*X*the value of*false*can remove the clauses containing*X=false*. - If
*X*is assigned the value of*true*, any clause with*X=false*can be simplified by removing*X=false*from the clause. Similarly, if*X*is assigned the value of*false*, then*X=true*can be removed from any clause it appears in. This step is called**unit resolution**.

Following some steps of pruning the clauses, clauses may exist that contain just one
assignment, *Y=v*. In this case, the other value can be removed from the
domain of *Y*. The aforementioned procedure can be repeated for the
assignment of *Y=v*. If all of the assignments are removed from a
clause, the constraints are unsatisfiable.

**Example 4.23:**Consider the clause

*¬x∨ y ∨ ¬z*. When

*X*is assigned to

*true*, the clause can be simplified to

*y ∨ ¬z*. If

*Y*is then assigned to

*false*, the clause can be simplified to

*¬z*. Thus,

*true*can be pruned from the domain of

*Z*.

If, instead, *X* is assigned to *false*, the preceding clause can be removed.

If a variable has the same value in all remaining
clauses, and the algorithm must only find one model, it can assign that value to that
variable. For example, if variable *Y* only appears as
*Y=true* (i.e., * ¬y* is not in any clause), then *Y* can be
assigned the value *true*. That assignment does not remove all of the models; it
only simplifies the problem because the set of clauses
remaining after setting *Y=true* is a subset of the clauses that
would remain
if *Y* were assigned the value *false*. A variable that only has one value in all
of the clauses is called a **pure symbol**.

It turns out that pruning the domains and constraints, domain
splitting, assigning
pure symbols, and
efficiently managing the constraints (i.e., determining when
all but one of the disjuncts are false) turns out to be a very
efficient algorithm. It is called the **DPLL** algorithm, after its authors.