Constructing Conditional Plans by a Theorem-Prover

Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite dierent from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisability algorithms in classical planning. Translating conditional planning to formulae in the propositional logic is not feasible because of inherent computational limitations. Instead, we translate conditional planning to quantied Boolean formulae. We discuss three formalizations of conditional planning as quantied Boolean formulae, and present experimental results obtained with a theorem-prover. Plans consist of operators that make a set of facts true whenever their preconditions are fullled. The most basic { and the most common in earlier research { form of plans is sequence of operators that are executed unconditionally in the specied order. Plans of this form are sucient only if the world where a plan is carried out is completely predictable and known, and the execution of the plan always starts in the same state. When not all changes in the world can be predicted or not all facts aecting plan execution are known in advance, the structure of plans has to be more general. If the task is to move object A, that is in room 1 or in room 2, to a trash can, the operations that achieve the goal depend on the initial location of A. There is no single sequence of operations that achieves the goal in both cases.