theorem prover implementation. or e ample for the problems in Table , na ve e tensions consider all of the  " truth value assignments to ol and the universally uantified variables ust to verify that a plan that has been found actually reaches the goal in all cases. urther developments in theorem proving techni ues for and propositional satisfiability are likely to improve these runtimes further.

## 8. Related Work

oth Peot and   mith and Pryor and ollins present algorithms for conditional planning that are based on the least commitment or partial order planning paradigm.    oth algorithms work like corresponding classical planning algorithms until a subgoal is fulfilled by the application of an operator that does not have a uni_ue outcome, that is, the operator is nondeterministic.   t that point the development of the conditional plan is split to a nmber of separate subproblems that are solved separately, each corresponding to one of the outcomes of the nondeterministic operator. The problem with this approach is that the si es of conditional plans are e  ponential on the number of uncertainties, and as generating a solution takes at best linear time on the si e of the solution  usually e ponential , this kind of algorithms inherently consume a lot of computational resources.    urthermore, often the improvement over the trivial conditional planning algorithm that simply reduces the problem to a number of classical planning problems that are solved separately, is small.  They fare better than the trivial algorithm whenever some of the contingencies are irrelevant in reaching the goal, or if the separate plans have parts in common.

imatti et al.

propose an algorithm for conditional planning that enumerates the state space. tarting from the goal states, the sets of states from which a goal state is reachable with 0 steps or less are computed.    hen for some   the set includes all initial states, a plan has been found.   uring the enumeration, each state is associated with an operation that is along a shortest path to a goal state.  Now the goals can be reached from any of the initial states by repeatedly applying the operator associated with the current state. s the number of state action pairs in these plans is as high as the nmber of states, problem instances with big state spaces consume more memory than is likely to be available. To alleviate this problem  imatti et al. propose the use of binary decision diagrams   ryant, for encoding the state action tables.

s are in general not capable of representing e  ponential si e data structures in polynomial space.

mith and eld e tend Graphplan   lum urst, to handle uncertainty and several initial states. The plans produced by their planner are se uences of operators like in classical planning, but as the e ects of operators may be conditional on some facts, the plans may achieve the goals even when starting the plan e ecution in di erent states or when there is nondeterminism.  mith and   eld call this conformant planning.  Their planning algorithm e plicitly represents information on all e ecutions of a plan. This may be possible when the number of initial states is small, up to a couple of do en or a hundred on small problem instances, but for more comple  problems it is not feasible because of high memory consumption.   epresenting conformant planning in our framework is easy.

Our work and satisfiability planning by  aut  and  elman are closely ma or di  erence is that we can directly address a much wider range of planning related.

problems with nondeterministic change and several initial states.   ecause of the added