foundations of computational agents
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 . If is a Boolean variable, we write as its lower-case equivalent, , and write as . Thus, given a Boolean variable Happy, the proposition happy means , and means .
Clausal constraints: a clause is an expression of the form , where each 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 appear in a clause, the atom is said to appear negatively in the clause. If 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 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 , , living violates the constraint of clause . 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 with domain can be converted into Boolean variables , where is true when has value and is false otherwise. Each is called an indicator variable. Thus atoms, , are used to represent the CSP variable.
There are constraints that specify that and cannot both be true when . There is a constraint that one of the must be true. Thus, the knowledge base contains the clauses: for and .
There is a clause for each false assignment in each constraint, which specifies which assignments to the are not allowed by the constraint. Often these clauses can be combined resulting in simpler constraints. For example, the clauses and can be combined to .