Another interesting approach is to convert the planning problem into
an enormous Boolean satisfiability problem. This means that the
planning problem of Formulation 2.4 can be solved by
determining whether some assignment of variables is possible for a
Boolean expression that leads to a TRUE value. Generic methods for
determining satisfiability can be directly applied to the Boolean
expression that encodes the planning problem. The *Davis-Putnam
procedure* is one of the most widely known algorithms for
satisfiability. It performs a depth-first search by iteratively
trying assignments for variables and backtracking when assignments
fail. During the search, large parts of the expression can be
eliminated due to the current assignments. The algorithm is complete
and reasonably efficient. Its use in solving planning problems is
surveyed in [382]. In practice, stochastic local search
methods provide a reasonable alternative to the Davis-Putnam procedure
[459].

Suppose a planning problem has been given in terms of Formulation
2.4. All literals and operators will be tagged with a
stage index. For example, a literal that appears in two different
stages will be considered distinct. This kind of tagging is similar
to *situation calculus* [378]; however, in that case,
variables are allowed for the tags. To obtain a finite, Boolean
expression the total number of stages must be declared. Let
denote the number of stages at which operators can be applied. As
usual, the fist stage is and the final stage is
.
Setting a stage limit is a significant drawback of the approach
because this is usually not known before the problem is solved. A
planning algorithm can assume a small value for and then gradually
increase it each time the resulting Boolean expression is not
satisfied. If the problem is not solvable, however, this approach
iterates forever.

Let denote logical OR, and let denote logical AND.
The Boolean expression is written as a
conjunction^{2.5} of many
terms, which arise from five different sources:

**Initial state:**A conjunction of all literals in is formed, along with the negation of all positive literals not in . These are all tagged with , the initial stage index.**Goal state:**A conjunction of all literals in , tagged with the final stage index, .**Operator encodings:**Each operator must be copied over the stages. For each , let denote the operator applied at stage . A conjunction is formed over all operators at all stages. For each , the expression is(2.33)

in which , , are the preconditions of , and , , are the effects of .**Frame axioms:**The next part is to encode the implicit assumption that every literal that is not an effect of the applied operator remains unchanged in the next stage. This can alternatively be stated as follows: If a literal becomes negated to , then an operator that includes as an effect must have been executed. (If was already a negative literal, then is a positive literal.) For each stage and literal, an expression is needed. Suppose that and are the same literal but are tagged for different stages. The expression is(2.34)

in which , , are the operators, tagged for stage , that contain as an effect. This ensures that if appears, followed by , then some operator must have caused the change.**Complete exclusion axiom:**This indicates that only one operator applies at every stage. For every stage , and any pair of stage-tagged operators and , the expression is(2.35)

which is logically equivalent to (meaning, ``not both at the same stage'').

The following example illustrates the construction.

The expression for the initial state is

(2.36) |

which uses the abbreviated names, and the stage tag has been added as an argument to the predicates. The expression for the goal state is

(2.37) |

which indicates that the goal must be achieved at stage . This value was determined because we already know the solution plan from (2.24). The method will also work correctly for a larger value of . The expressions for the operators are

(2.38) |

for each from to .

The frame axioms yield the expressions

(2.39) |

for each from to . No operators remove batteries from the flashlight. Hence, two of the expressions list no operators.

Finally, the complete exclusion axiom yields the expressions

(2.40) | ||||||

for each from to . The full problem is encoded by combining all of the given expressions into an enormous conjunction. The expression is satisfied by assigning TRUE values to , , , and . An alternative solution is , , , and . The stage index tags indicate the order that the actions are applied in the recovered plan.

Steven M LaValle 2012-04-20