5 Propositions and Inference 5.1 Propositions 5.3 Propositional Definite Clauses

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 $\neg{x}$ .

For example, the proposition ${happy}$ means Boolean variable ${Happy}$ is true ( ${Happy}{\,{=}\,}{true}$ ), and $\neg{{happy}}$ means ${Happy}{\,{=}\,}{false}$ .
•

Clausal constraints. A clause is an expression of the form $l_{1}\vee l_{2}\vee\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 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 $\neg 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 $l_{1}\vee l_{2}\vee\dots\vee l_{k}$ corresponds to the statement $\neg(\neg l_{1}\land\neg l_{2}\land\dots\land\neg l_{k})$ , which says that not all of the $l_{i}$ are false.

Example 5.4.

The clause ${happy}\vee{sad}\vee\neg{{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 $\neg{{happy}}$ , $\neg{{sad}}$ , ${{living}}$ violates the constraint of clause ${happy}\vee{sad}\vee\neg{{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 $\{v_{1},\dots,v_{k}\}$ can be converted into $k$ Boolean variables $\{Y_{1},\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},\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\neq j$ , namely the clause $\neg y_{i}\lor\neg y_{j}$ for $i<j$ . There is also a constraint that one of the $y_{i}$ must be true, namely the clause $y_{1}\lor\dots\lor y_{k}$ .
•

To translate the constraints, notice that $\neg x_{1}\lor\dots\lor\neg x_{k}$ is equivalent to $\neg(x_{1}\land\dots\land x_{k})$ for any atoms $x_{1},\dots,x_{k}$ . 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 $\neg x_{5}\lor\neg y_{7}$ represents that $X{\,{=}\,}v_{5}$ and $Y{\,{=}\,}v_{7}$ 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 $a_{1}$ , $a_{2}$ , $a_{3}$ , and $a_{4}$ , where $a_{1}$ is true just when $A{\,{=}\,}1$ , $a_{2}$ is true just when $A{\,{=}\,}2$ , etc. Variables $a_{1}$ , $a_{2}$ , $a_{3}$ , and $a_{4}$ are disjoint and covering which leads to the seven clauses

	$\displaystyle\neg a_{1}\vee\neg a_{2},\neg a_{1}\vee\neg a_{3},\neg a_{1}\vee% \neg a_{4},\neg a_{2}\vee\neg a_{3},\neg a_{2}\vee\neg a_{4},\neg a_{3}\vee% \neg a_{4},$
	$\displaystyle a_{1}\vee a_{2}\vee a_{3}\vee a_{4}.$

Similarly for $B$ .

The constraint $A<B$ implies that $a_{4}$ is false, $b_{1}$ is false, and the pairs that violate the constraint are also false, which gives the five clauses

\displaystyle\neg a_{4},\neg b_{1},\neg a_{2}\vee\neg b_{2},\neg a_{3}\vee\neg b% _{3},\neg a_{3}\vee\neg b_{2}.

Note that you don’t need the clause $\neg a_{1}\vee\neg b_{1}$ because this is implied by $\neg b_{1}$ .

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 $\neg{x}\vee y\vee\neg{z}$ . If $X$ is assigned to ${true}$ , the clause can be simplified to $y\vee\neg{z}$ . If $Y$ is then assigned to ${false}$ , the clause can be simplified to $\neg{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., $\neg{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.

Artificial Intelligence 3E