Parallel encodings of classical planning as satisfiability

Reference:

Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Parallel encodings of classical planning as satisfiability. Technical Report 198, Institute of Computer Science, University of Freiburg, Freiburg, Germany, February 2004.

Abstract:

We consider a number of semantics for plans with parallel operator application. The standard semantics used most often in earlier work requires 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, first proposed outside planning in connection with Petri nets. We formalize the semantics of parallel plans emerging in this setting, propose effective translations of the sesemantics 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.

Keywords:

planning, propositional logic, satisfiability testing

Suggested BibTeX entry:

@techreport{RinHelNie:TR198,
    address = {Freiburg, Germany},
    author = {Jussi Rintanen and Keijo Heljanko and Ilkka Niemel{\"a}},
    institution = {Institute of Computer Science, University of Freiburg},
    month = {February},
    number = {198},
    pages = {8},
    title = {Parallel encodings of classical planning as satisfiability},
    type = {Technical Report},
    year = {2004},
}