generality, the problems we can solve do not in general belong to the comple ity class NP. f all sources of uncertainty are eliminated, our translations contain only e istential untifiers, and these   uantified   oolean formulae are true e  actly when the same formulae without the   uantifiers are satisfiable.  Our translations in these cases still contain the more comple  representation of conditional plans, but otherwise the resulting sets of formulae are similar and plans can be found by a satisfiability algorithm.

fundamental di  erence between the satisfiability algorithms of    aut   and   elman and our theorem prover is that the former, GSAT and WALKSAT, are based on local search.

These algorithms repeatedly try to guess truth value assignments that satisfy the set of clauses.   t no point of time is there a guarantee that all assignments have been considered, and therefore these algorithms are not capable of determining the unsatisfiability of a set of clauses.  n general, because local search algorithms do not e haustively go through the search space, they cannot determine with certainty that an ob ect with a certain property does not e  ist.     local search algorithm can find a conditional plan but it cannot determine its correctness.

ithout systematically considering all combinations of contingencies, only countere amples that show a plan incorrect can be found. Therefore at least those parts of algorithms for conditional planning that verify that a plan is correct have to be systematic.

## 9. Conclusions And Future Work

e propose a new approach to conditional planning that is based on representing problem instances as uantified oolean formulae and using an automated theorem prover for finding plans. This approa is both theoretically and practically well motivated.   s a practical motivation we see the recent success of satisfiability algorithms and elman, in classical planning. The problem of determining truth values of   uantified    oolean formulae is a generali  ation of the problem of satisfiability of propositional formulae.    s a theoretical ustification we give comple ity results that demonstrate that it is in general not feasible to use satisfiability algorithms in conditional planning.

This work di ers from earlier work on conditional planning in several respects. Unlike the planning algorithms   NLP and   assandra  Peot      mith,
: Pryor ollins, we do not reduce conditional planning to the simpler case of planning without uncertainties.

s shown by our theoretical analysis, this reduction would be ill motivated, as it most likely cannot be done in polynomial time.   n some cases when finding a plan is easy, this reduction makes it very costly.   imatti et al.

give an algorithm that enumerates the state space of a conditional planning problem.  The plans constructed by their algorithm e  plicitly associate an operation with every state, and this inherently leads to big plans.  t is not clear whether the techni ues they propose make this feasible for comple  problems.

e have developed a prototype implementation of a theorem prover for and e perimented with producing conditional plans with it. The results are preliminary, but give a  ustification to our approach  simple benchmark problems that would be far too di  cult for some of the earlier conditional planners are  uickly solved in time that is sublinear on the number of initial states in the problem instances.    e believe that e pressing condi tional planning as a theorem proving task makes it easier to identify general techni  ues that benefit the construction of conditional plans, and also to identify techni  ues that cannot be conveniently embedded in particular theorem proving frameworks.