# Pseudo-Boolean Proof Logging for Optimal Classical Planning

arXiv: https://arxiv.org/abs/2504.18443 · HTML: https://mlsanity.com/paper/2504.18443/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 28 references that are in the map.
- First posted on arXiv 25 Apr 2025.

## Builds on (most cited first, 2 of 2)

- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)

## Abstract (arXiv)

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^textitmax as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.