Technical Report No. 216 - Abstract

Jussi Rintanen, Keijo Heljanko, Ilkka Niemela
Planning as satisfiability: parallel plans and algorithms for plan search

We address two aspects of constructing plans efficiently by means of satisfiability testing: efficient encoding of the problem of existence of plans of a given number t of time points in the propositional logic, and strategies for finding plans given the formulae representing these formulae for different values of t. For the first problem we consider a number of semantics for plans with parallel operator application. The standard semantics used most often in earlier work require that parallel operators are independent and can therefore be executed in any order. We consider a more relaxed definition of parallel plans, first proposed by Dimopoulos et al., as well as normal forms for parallel plans that require every operator to be executed as early as possible. We formalize the semantics of parallel plans emerging in this setting, and present translations of these semantics into the propositional logic. The sizes of the translations are asymptotically optimal. For the second problem we consider strategies based on testing the satisfiability of several formulae representing plans of n time steps for several values of n concurrently by several processes. We show that big efficiency gains can be obtained in comparison to the standard strategy of sequentially testing the satisfiability of formulae for an increasing number of time steps.