Formalization of Lower-Bound Certificates for Optimal Classical Planning

We formalize the framework of pseudo-Boolean lower-bound certificates for classical planning introduced by Dold, Helmert, Nordström, Röger and Schindler. A lower-bound certificate for a STRIPS (Simplified Theory of International Planning Representation and Scheduling) planning task and a bound $B$ is a pseudo-Boolean circuit together with three proofs in the cutting planes proof system with reification; its validity guarantees that every plan of the task costs at least $B$, and hence that a plan of cost $B$ is optimal. We prove the soundness of the certificate format (Theorem 1 of the paper) and formalize the paper's case study: certificates extracted from a run of the A$^*$ algorithm, with heuristic certificates for pattern database heuristics and for the maximum heuristic $h^{\mathit{max}}$, including the appendix material on efficiently proof-logging pattern databases. The main results state that a suitable snapshot of a terminated A$^*$ run yields a valid certificate and therefore proves the optimality of the plan it found. All locales are shown consistent by concrete interpretations, which also compose the pattern database certificate with the A$^*$ certificate, as intended by the paper.