Unsolvability Certificates for Classical Planning

Authors

  • Salomé Eriksson University of Basel
  • Gabriele Röger University of Basel
  • Malte Helmert University of Basel

DOI:

https://doi.org/10.1609/icaps.v27i1.13818

Abstract

The plans that planning systems generate for solvable planning tasks are routinely verified by independent validation tools. For unsolvable planning tasks, no such validation capabilities currently exist. We describe a family of certificates of unsolvability for classical planning tasks that can be efficiently verified and are sufficiently general for a wide range of planning approaches including heuristic search with delete relaxation, critical-path, pattern database and linear merge-and-shrink heuristics, symbolic search with binary decision diagrams, and the Trapper algorithm for detecting dead ends. We also augmented a classical planning system with the ability to emit certificates of unsolvability and implemented a planner-independent certificate validation tool. Experiments show that the overhead for producing such certificates is tolerable and that their validation is practically feasible.

Downloads

Published

2017-06-05

How to Cite

Eriksson, S., Röger, G., & Helmert, M. (2017). Unsolvability Certificates for Classical Planning. Proceedings of the International Conference on Automated Planning and Scheduling, 27(1), 88-97. https://doi.org/10.1609/icaps.v27i1.13818