Martin Kronegger, Andreas Pfandler and Reinhard Pichler
Conformant Planning as a Benchmark for QBF-Solvers
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.