Pseudo-Boolean Proof Logging for Optimal Classical Planning
This provides a method for trustworthy verification in planning, which is incremental as it builds on existing heuristic frameworks.
The paper tackles the problem of verifying optimality or unsolvability in classical planning tasks by introducing lower-bound certificates based on pseudo-Boolean constraints, enabling independent verification with modest overhead in algorithms like A*.
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 $h^\textit{max}$ as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.