Optimality Certificates for Classical Planning


  • Esther Mugdan University of Basel, Switzerland
  • Remo Christen University of Basel, Switzerland
  • Salomé Eriksson University of Basel, Switzerland




Classical planning techniques and analysis, Theoretical foundations of planning and scheduling, Heuristic search


Algorithms are usually shown to be correct on paper, but bugs in their implementations can still lead to incorrect results. In the case of classical planning, it is fortunately straightforward to check whether a computed plan is correct. For optimal planning however, plans are additionally required to have minimal cost, which is significantly more difficult to verify. While some domain-specific approaches exists, we lack a general tool to verify optimality for arbitrary problems. We bridge this gap and introduce two approaches based on the principle of certifying algorithms, which provide a computer-verifiable certificate of correctness alongside their answer. We show that both approaches are sound and complete, analyze whether they can be generated and verified efficiently, and show how to apply them to concrete planning algorithms. The experimental evaluation shows that verifying optimality comes with a cost but is still practically feasible. Furthermore it confirms that the tested planner configurations provide optimal plans on the given instances, as all certificates were verified successfully.




How to Cite

Mugdan, E., Christen, R., & Eriksson, S. (2023). Optimality Certificates for Classical Planning. Proceedings of the International Conference on Automated Planning and Scheduling, 33(1), 286-294. https://doi.org/10.1609/icaps.v33i1.27206