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

The class of propositional satisfiability problems have:

• •

  Boolean variables: a Boolean variable is a variable with domain $\{\text{true},\text{false}\}$. If $X$ is a Boolean variable, we write $X=\text{true}$ as its lower-case equivalent, $x$, and write $X=\text{false}$ as $\mathrm{\neg }x$. Thus, given a Boolean variable Happy, the proposition happy means $\text{Happy}=\text{true}$, and $\mathrm{\neg }\text{happy}$ means $\text{Happy}=\text{false}$.

• •

  Clausal constraints: a clause is an expression of the form $l_1\vee l_2\vee \mathrm{\dots }\vee l_k$, where each $l_i$ 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 satisfied 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.

  If $\mathrm{\neg }a$ appear 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 formulas. Any propositional formula can be converted into clausal form.

In terms of constraints, a clause is a constraint on a set of Boolean variables that rules out one of the assignments from consideration – the assignment that makes all literals false.

It is possible to convert any finite CSP into a propositional satisfiable problem:

• •

  A CSP variable $Y$ with domain $\{v_1,\mathrm{\dots },v_k\}$ can be converted into $k$ Boolean variables $\{Y_1,\mathrm{\dots },Y_k\}$, where $Y_i$ is true when $Y$ has value $v_i$ and is false otherwise. Each $Y_i$ is called an indicator variable. Thus $k$ atoms, $y_1,\mathrm{\dots },y_k$, are used to represent the CSP variable.

• •

  There are constraints that specify that $y_i$ and $y_j$ cannot both be true when $i\ne j$. There is a constraint that one of the $y_i$ must be true. Thus, the knowledge base contains the clauses: $\mathrm{\neg }{y}_i\vee \mathrm{\neg }{y}_j$ for and $y_1\vee \mathrm{\dots }\vee y_k$.

• •

  There is a clause for each false assignment in each constraint, which specifies which assignments to the $Y_i$ are not allowed by the constraint. Often these clauses can be combined resulting in simpler constraints. For example, the clauses $a\vee b\vee c$ and $a\vee b\vee \mathrm{\neg }c$ can be combined to $a\vee b$.