foundations of computational agents
The third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including full text).
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.
The clause ${\text{\u210e\mathit{a}\mathit{p}\mathit{p}\mathit{y}}}{\mathrm{\vee}}{\text{\mathit{s}\mathit{a}\mathit{d}}}{\mathrm{\vee}}{\mathrm{\neg}}{\mathit{}}{\text{\mathit{l}\mathit{i}\mathit{v}\mathit{i}\mathit{n}\mathit{g}}}$ 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 ${\mathrm{\neg}}{\mathit{}}{\text{\u210e\mathit{a}\mathit{p}\mathit{p}\mathit{y}}}$, ${\mathrm{\neg}}{\mathit{}}{\text{\mathit{s}\mathit{a}\mathit{d}}}$, living violates the constraint of clause ${\text{\u210e\mathit{a}\mathit{p}\mathit{p}\mathit{y}}}{\mathrm{\vee}}{\text{\mathit{s}\mathit{a}\mathit{d}}}{\mathrm{\vee}}{\mathrm{\neg}}{\mathit{}}{\text{\mathit{l}\mathit{i}\mathit{v}\mathit{i}\mathit{n}\mathit{g}}}$. It is the only assignment of these three variables that violates this clause.
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$.