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 $\{\text{true},\text{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=\text{true}$ become redundant; they are automatically satisfied. These clauses can be removed. Similarly, if $X$ is assigned false, clauses containing $X=\text{false}$ can be removed.

• •

  If $X$ is assigned true, any clause with $X=\text{false}$ can be simplified by removing $X=\text{false}$ from the clause. Similarly, if $X$ is assigned false, then $X=\text{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.

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=\text{true}$ (i.e., $\mathrm{\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=\text{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.