5.2 Propositional Constraints

Chapter 4 shows how to reason with constraints. Logical formulas provide a concise form of constraints with structure that can be exploited.

There are a number of reasons for using propositions for specifying constraints and queries:

  • It is often more concise and readable to give a logical statement about the relationship among some variables than to use an extensional representation.

  • The form of the knowledge can be exploited to make reasoning more efficient.

  • They are modular, so small changes to the problem result in small changes to the knowledge base. This also means that a knowledge base is easier to debug than other representations.

  • The kind of queries may be richer than single assignments of values to variables.

  • This language can be extended to reason about individuals (things, entities) and relations; see Chapter 15.

The class of propositional satisfiability or SAT problems have

  • Boolean variable. A Boolean variable is a variable with domain {true,false}. If X is a Boolean variable, X=true is written as its lower-case equivalent, x, and X=false as ¬x.

    For example, the proposition happy means Boolean variable Happy is true (Happy=true), and ¬happy means Happy=false.

  • Clausal constraints. A clause is an expression of the form l1l2lk, where each li is a literal. A literal is an atom or the negation of an atom; thus a literal is an assignment of a value to a Boolean variable. A clause is true in an interpretation if and only if at least one of the literals that make up the clause is true in that interpretation.

    If ¬a appears in a clause, the atom a is said to appear negatively in the clause. If a appears unnegated in a clause, it is said to appear positively in a clause.

In terms of the propositional calculus, a set of clauses is a restricted form of logical formula. Any propositional formula can be converted into clausal form. A total assignment corresponds to an interpretation.

In terms of constraints, a clause is a constraint on a set of Boolean variables that rules out one of the assignments of the literals in the clause. The clause l1l2lk corresponds to the statement ¬(¬l1¬l2¬lk), which says that not all of the li are false.

Example 5.4.

The clause happysad¬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. The atoms happy and sad appear positively in the clause, and living appears negatively in the clause.

The assignment ¬happy, ¬sad, living violates the constraint of clause happysad¬living. It is the only assignment of these three variables that violates this clause.

5.2.1 Clausal Form for CSPs

It is possible to convert any finite constraint satisfaction problem (CSP) into a propositional satisfiable problem:

  • A variable Y with domain {v1,,vk} can be converted into k Boolean variables {Y1,,Yk}, where Yi is true when Y has value vi and is false otherwise. Each Yi is called an indicator variable. Thus, k atoms, y1,,yk, are used to represent the CSP variable.

  • There are constraints that specify that yi and yj cannot both be true when ij, namely the clause ¬yi¬yj for i<j. There is also a constraint that one of the yi must be true, namely the clause y1yk.

  • To translate the constraints, notice that ¬x1¬xk is equivalent to ¬(x1xk) for any atoms x1,,xk. One way to represent a constraint is to use a clause for each assignment of values that violates the constraint. Thus, for example, the clause ¬x5¬y7 represents that X=v5 and Y=v7 is a combination that violates a constraint.

    Often we can use many fewer clauses than by applying this naively.

Example 5.5.

Consider two variables A and B each with domain {1,2,3,4}. For the variable A, construct four Boolean variables a1, a2, a3, and a4, where a1 is true just when A= 1, a2 is true just when A= 2, etc. Variables a1, a2, a3, and a4 are disjoint and covering which leads to the seven clauses


Similarly for B.

The constraint A<B implies that a4 is false, b1 is false, and the pairs that violate the constraint are also false, which gives the five clauses


Note that you don’t need the clause ¬a1¬b1 because this is implied by ¬b1.

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 a 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 from consideration. 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.6.

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.

Pruning the domains and constraints, domain splitting, and assigning pure literals is the Davis–Putnam–Logemann–Loveland (DPLL) algorithm. It is a very efficient algorithm, as long as the data structures are indexed to carry out these tasks efficiently.

5.2.2 Exploiting Propositional Structure in Local Search

Stochastic local search can be faster for CSPs in the form of propositional satisfiability problems than for general CSPs, for the following reasons:

  • Because only one alternative value exists for each assignment to a variable, the algorithm does not have to search through the alternative values.

  • Changing any value in an unsatisfied clause makes the clause satisfied. As a result, it is easy to satisfy a clause, but this may make other clauses unsatisfied.

  • If a variable is changed to be true, all of the clauses where it appears positively become satisfied, and only clauses where it appears negatively can become unsatisfied. Conversely, if a variable is changed to be false, all of the clauses where it appears negatively become satisfied, and only those clauses where it appears positively can become unsatisfied. This enables fast indexing of clauses.

  • The search space is expanded. In particular, before a solution has been found, more than one of the indicator variables for a variable Y could be true (which corresponds to Y having multiple values) or all of the indicator variables could be false (which corresponds to Y having no values). This can mean that some assignments that were local minima in the original problem may not be local minima in the new representation.

  • Satisfiability has been studied much more extensively than most other types of CSPs and more efficient solvers exist because more of the space of potential algorithms has been explored by researchers.

Whether converting a particular CSP to a satisfiability problem makes search performance better is an empirical question, depending on the problem and the tools available.