Tanja Schindler – Publications

(Show all abstracts) (Hide all abstracts)

2025

Simon Dold, Malte Helmert, Jakob Nordström, Gabriele Röger and Tanja Schindler.
Pseudo-Boolean Proof Logging for Optimal Classical Planning.
In Proceedings of the 35th International Conference on Automated Planning and Scheduling (ICAPS 2025), pp. 54-63. 2025.
(Show abstract) (Hide abstract) (PDF) (extended version) (slides; PDF)

We introduce lower-bound certificates for classical planning tasks, which can be used to prove the unsolvability of a task or the optimality of a plan in a way that can be verified by an independent third party. We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints, which is agnostic to the planning algorithm used. As a case study, we show how to modify the A∗ algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and hmax as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.