Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).

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 l1∨ l2 ∨ ...∨ lk, where each li is a literal. A 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.