Unsolvability Certificates for Classical Planning

Eriksson, Salomé and Röger, Gabriele and Helmert, Malte. (2017) Unsolvability Certificates for Classical Planning. In: Proceedings of the 27th International Conference on Automated Planning and Scheduling (ICAPS 2017).

[img] PDF - Published Version

Official URL: https://edoc.unibas.ch/59251/

Downloads: Statistics Overview


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.
Faculties and Departments:05 Faculty of Science > Departement Mathematik und Informatik > Informatik > Artificial Intelligence (Helmert)
UniBasel Contributors:Eriksson, Salomé and Röger, Gabriele and Helmert, Malte
Item Type:Conference or Workshop Item, refereed
Conference or workshop item Subtype:Conference Paper
Publisher:AAAI Press
Note:Publication type according to Uni Basel Research Database: Conference paper
Related URLs:
edoc DOI:
Last Modified:09 Feb 2018 15:14
Deposited On:09 Feb 2018 15:14

Repository Staff Only: item control page