Inductive Certificates of Unsolvability for Domain-Independent Planning

Inductive Certificates of Unsolvability for Domain-Independent Planning

Salomé Eriksson, Gabriele Röger, Malte Helmert

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 5244-5248. https://doi.org/10.24963/ijcai.2018/730

If a planning system outputs a solution for a given problem, it is simple to verify that the solution is valid. However, if a planner claims that a task is unsolvable, we currently have no choice but to trust the planner blindly. We propose a sound and complete class of certificates of unsolvability which can be verified efficiently by an independent program. To highlight their practical use, we show how these certificates can be generated for a wide range of state-of-the-art planning techniques with only polynomial overhead for the planner.
Keywords:
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
Planning and Scheduling: Theoretical Foundations of Planning