# 5.2.1 Clausal Form for Consistency Algorithms

Consistency algorithms can be made more efficient for propositional satisfiability problems than for general CSPs. When there are only two values, pruning a value from the domain is equivalent to assigning the opposite value. Thus, if $X$ has domain $\{\mbox{true},\mbox{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=\mbox{true}$ become redundant; they are automatically satisfied. These clauses can be removed. Similarly, if $X$ is assigned false, clauses containing $X=\mbox{false}$ can be removed.

• If $X$ is assigned true, any clause with $X=\mbox{false}$ can be simplified by removing $X=\mbox{false}$ from the clause. Similarly, if $X$ is assigned false, then $X=\mbox{true}$ can be removed from any clause it appears in. This step is called unit resolution.

If, after pruning the clauses, there is a clause that contains just one assignment, $Y=v$, the other value can be removed from the domain of $Y$. This is a form of arc consistency. If all of the assignments are removed from a clause, the constraints are unsatisfiable.

###### Example 5.5.

Consider the clause $\neg{x}\vee y\vee\neg{z}$. If $X$ is assigned to true, the clause can be simplified to $y\vee\neg{z}$. If $Y$ is then assigned to false, the clause can be simplified to $\neg{z}$. Thus, true can be pruned from the domain of $Z$.

If, instead, $X$ is assigned to false, the 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=\mbox{true}$ (i.e., $\neg{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=\mbox{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 literal.

It turns out that pruning the domains and constraints, domain splitting, and assigning pure literals is a very efficient algorithm, as long as the data structures are indexed to carry out these tasks efficiently. It is called the DPLL algorithm, after its authors.