
| encoding   | blocks   | value   |         |       |         |       |
|------------|----------|---------|---------|-------|---------|-------|
| istates    | time     | states  | clauses | vars  | runtime | nodes |
| 0.         | 0        | false   |         |       |         |       |
| s          |          |         |         |       |         |       |
| s          | false    |         |         |       |         |       |
| true       |          |         |         |       |         |       |
| s          | false    |         |         |       |         |       |
| 0.         | s        | 0       |         |       |         |       |
| 0          | 0.       | s       | 0       | false |         |       |
| 0          | true     |         |         |       |         |       |
| 0          | s        |         |         |       |         |       |
| 0          | 0.0 s    | 0       | false   |       |         |       |
| S          | true     |         |         |       |         |       |
| false      |          |         |         |       |         |       |
| .0 s       | 0        |         |         |       |         |       |
| h          | ?        | ?       |         |       |         |       |
| ?          | ?        |         |         |       |         |       |
| h          | false    |         |         |       |         |       |
| 0          | s        | 0       |         |       |         |       |
| 0          | 0        | false   |         |       |         |       |
| s          |          |         |         |       |         |       |
| 0          | s        | 0       | true    |       |         |       |
| 0          | false    |         |         |       |         |       |
| s          |          |         |         |       |         |       |
| 0          | .0 s     | 0       | true    |       |         |       |

Ta ble e ample with the plan encoding from  ection . .  than with the simpler encoding from ection . . may therefore be surprising. The di  erence would seem to be due to the fact that the low number of internal states three in the plans from ection . . forces the plan to stay  in some of the states for several points of time.   or plans from   ection  .  .   there is no such restriction and the sets of operators enabled at each point of time may be di_erent.

The constraints on solution plans are therefore not as tight for the simpler representation, and more search is needed for finding a plan.

ith these blocks world problem instances the solution of the separate problems is very easy for the best classical planners.    hat makes these problems di  cult is that the plans represent all possible e ecutions, and the constraints on the plans are not as tight as in the benchmarks in Table or in the separate classical planning problems. owever, when considering that the number of elements in the resulting plans is relatively high  fifteen or more for the bigger problems  and the notion of plans is much more complicated than in classical planning, the runtimes are not disappointing.

oe of the observations about plan search in our approach are interesting.    ven though there are three  uantifiers, our theorem prover does not perform search on variables  uan tified by the third one that represent plan e  ecutions. This is because the plan, represented by the outermost variables, together with the universally  uantified variables for the con tingencies, uni uely determine the ecution that is found without search. This is nicely on par with the fact that conditional planning is on the second level of the polynomial hierarchy, not on the third as the prefi 3V3 in the encodings might suggest.

s shown in Table   , the runtimes for plan generation can be much less than linear to the nmber of initial states.  None of the early conditional planning algorithms is able to e  hibit similar behavior; that is, they produce plans of e ponential length and therefore consume e ponential time even on simple problems like these. The favorable runtimes are due to our