Technical Report No. 198 - Abstract

Jussi Rintanen, Keijo Heljanko, Ilkka Niemelä
Parallel Encodings of Classical Planning as Satisfiability

We consider a number of semantics for plans with parallel operator application. The standard semantics most often used in earlier work requires that parallel operators are independent, and can therefore 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, first proposed outside planning in connection with Petri nets. We formalize the semantics of parallel plans emerging in this setting, propose effective translations of these semantics to the classical propositional logic, and show that they yield an approach to classical planning that is often much more efficient than the existing SAT-based approaches.