foundations of computational agents
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 has domain , pruning true from the domain of is the same as assigning 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 is assigned true, all of the clauses with become redundant; they are automatically satisfied. These clauses can be removed. Similarly, if is assigned false, clauses containing can be removed.
If is assigned true, any clause with can be simplified by removing from the clause. Similarly, if is assigned false, then 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, , the other value can be removed from the domain of . This is a form of arc consistency. If all of the assignments are removed from a clause, the constraints are unsatisfiable.
Consider the clause . If is assigned to true, the clause can be simplified to . If is then assigned to false, the clause can be simplified to . Thus, true can be pruned from the domain of .
If, instead, 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 only appears as (i.e., is not in any clause), then 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 is a subset of the clauses that would remain if 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.