Pseudo-Boolean Proof Logging for Optimal Classical Planning

TL;DR

The paper tackles certifying optimality in classical planning by introducing lower-bound certificates built on pseudo-Boolean proofs and a cutting planes with reification proof system. It develops a general PB-based framework to encode planning tasks, express invariants, and verify that no plan cheaper than a bound $B$ exists, with separate init, inductivity, and goal proofs. A key contribution is the integration of proof-logging into heuristic search, notably in $A^*$, and the demonstration that certificates can be generated efficiently for both pattern database heuristics and $h^{\text{max}}$, yielding verifiable optimality proofs. The approach promises broad applicability and potential extension to cost-partitioning techniques, enabling independent verification of optimal planners across diverse planning paradigms.

Abstract

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.

Figures (1)

• Figure 1: Interaction of Components

Theorems & Definitions (33)

• Definition 1
• Definition 2
• Definition 3
• Theorem 1
• proof
• Lemma 1
• Lemma 2
• Definition 4
• Lemma 3
• proof