@inproceedings{KroneggerPP13-qbf,
  author    = {Martin Kronegger and Andreas Pfandler and Reinhard Pichler},
  title     = {Conformant Planning as a Benchmark for {QBF}-Solvers},
  booktitle = {Proc. of the International Workshop on Quantified Boolean Formulas (QBF 2013) colocated with SAT 2013},
  year      = {2013},
  editorOFF = {Florian Lonsing and Martina Seidl},
  pages     = {1--5}
  abstract  = {Planning is an important field of research in the area of artificial intelligence. Even one of the most basic cases of planning is NP-complete. However, this case assumes complete knowledge which in many practical settings is not available. The presence of incomplete knowledge leads to the case of so-called "conformant planning", whose complexity is on the second level of the polynomial hierarchy. It is thus a natural step to encode these planning problems as quantified Boolean formulas (QBFs). For this, several encodings have been proposed in the literature.
In this paper we present a framework for transforming conformant planning instances to QBFs in order to analyze how well QBF-solvers can handle planning problems. Since the planning instances are given in a non-ground modeling language several refinements are necessary to obtain QBFs of reasonable size. A key feature of this approach is that we aim at an "optimal plan", i.e., whenever a plan is found, its length is guaranteed to be minimal. The goal of this work is to gather some experience with this approach and highlight desiderata that could improve the performance and applicability of QBF-solvers in the area of planning.}
}