truth values obtained are ones that must be assigned to those variables.   econd, at any node of the search tree, if assigning true to and any truth values to some of the and then performing unit resolution yields a contradiction, then   has to be variables in assigned false. Third, detecting failed literals by unit resolution can also be performed on variables that cannot be chosen as the ne t branching variable, that is variables  uantified by some other than the current outermost   uantifier.

tion important research topic on reasoning with is how for a true formula with universally  uantified variables, going through all of the  n truth value assignments can be avoided. urrently the only techni ue we employ is partitioning clause sets at each node of the search tree so that no two sets have variables in common. or some planning is split to several clause sets with a low number of universal variables problems, the occurring in each, and this way the number of assignments that have to be considered is much less than  n

## 7. Experiments

e have written a program that translates conditional planning problems to
, and performed computational e periments in which conditional plans have been found by the theorem prover discussed in   ection l the translations are automatically generated from the set of operators and the formu le that describe the initial and goal states.  This program includes the automatic generation of invariants for the problem instance. The use of invariants erevini chubert, and related techni  ues for pruning search spaces is one of the distinguishing intanen, features of recent classical planners. y invariants we mean formulae that are true in all reachable states of a problem instance. nvariants are determined by the operators and the initial states, and they help plan search also in conditional planning.

e have run two series of benchmarks. The first benchmark demonstrates planning independent sources of uncertainty that corresponds to    problem instances with under out uncertainty.  The purpose of this benchmark is to demonstrate that it can be more natural and much easier to solve the whole conditional planning problem once, instead of solving the corresponding classical problem instances separately. The second benchmark is the blocks world with several initial states.    e let our theorem prover find a conditional plan that reaches a given goal state starting from every possible state. This benchmark is parameteri ed by the number of blocks, and we can solve the problem with blocks in a reasonable time.   or  ,   and   blocks the problem has respectively  0 ,  0 and initial states, and our translator has di culties in translating a representation of these states to clausal form.

The first scenario consists of a se uence of rooms with a pair of doors connecting con actly one door of each pair is open, and before e ecuting the plan it is secutive rooms.

not known which. The goal is to go from the first room to the last.

e ran this bench mark with the encoding from ection . . . n this case there is only one parameter that is increased during plan search, the length of the plan.   ence the theorem prover is first called with a formula that encodes plans/e ecutions of length  , then with a formula for length , and so on. rom the first formula that is found to be true a plan that reaches the goal can be e tracted. n Table we give statistics on the evaluation of formulae with