5.2 Propositional Constraints

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 {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, if X is assigned false, clauses containing X=false can be removed.

  • If X is assigned true, any clause with X=false can be simplified by removing X=false from the clause. Similarly, if X is assigned false, then X=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 ¬xy¬z. If 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 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 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.