Pseudo-Boolean Proof Logging for Optimal Classical Planning

📝 Paper Summary

Certifying Algorithms Automated Planning Formal Verification

Proposes a framework for certifying the optimality of classical planning solutions using pseudo-Boolean cutting planes proofs, enabling independent verification that no cheaper plan exists.

Core Problem

Classical planning algorithms claim to find optimal (cheapest) plans, but these claims are hard to verify without re-running the solver, and solvers may have bugs.

Why it matters:

Plan correctness is easy to verify (using tools like VAL), but verifying *optimality* (that no better plan exists) is currently unsolved for general cases.
Existing optimality certification methods are either inefficient (requiring exponential task reformulation) or too specific (limited to certain forward-search heuristics).
Blindly accepting solver outputs is risky in safety-critical applications; 'certifying algorithms' that produce proofs are standard in SAT but nascent in Planning.

Concrete Example: A planner outputs a plan $\pi$ with cost 10. A validator can check if $\pi$ works and costs 10. However, the validator cannot easily check if a hidden plan $\pi'$ with cost 9 exists. This paper generates a proof that cost < 10 leads to a contradiction.

Key Novelty

Pseudo-Boolean (PB) Cutting Planes with Reification for Planning

Encodes the planning task and heuristic estimates into pseudo-Boolean constraints (linear inequalities over boolean variables), which naturally handle arithmetic costs.
Uses a cutting planes proof system (supported by the VeriPB checker) to derive a contradiction for any goal state having a cost lower than the optimal plan.
Introduces 'heuristic certificates' that translate admissible heuristic values (like Pattern Databases) into PB constraints, allowing the proof to leverage heuristic information efficiently.

Architecture

The workflow of the certifying planning system

Breakthrough Assessment

8/10

Fills a major gap in reliable AI planning. While SAT certification is mature, general optimality certification for planning was missing. The move to Pseudo-Boolean (vs. CNF) is mathematically well-motivated for cost reasoning.

⚙️ Technical Details

Problem Definition

Setting: Optimal Classical STRIPS Planning

Inputs: Planning task $\Pi = \langle \mathcal{V}, \mathcal{A}, I, G \rangle$ (Variables, Actions, Initial State, Goal)

Outputs: Optimal Plan $\pi$ and an Optimality Certificate (Proof)

Pipeline Flow

Planner runs algorithm (e.g., A*) to find optimal plan
Planner generates Optimality Certificate (PB proof) alongside plan
Validator (e.g., VAL) checks plan correctness and cost
Verifier (VeriPB) checks Certificate against Task + Plan Cost

System Modules

Certifying Planner

Solves the task and logs proof steps justifying lower bounds on cost

Model or implementation: Modified A* Search (case study)

Plan Validator (Verification)

Checks that the generated plan is valid and calculates its cost

Model or implementation: VAL or INVAL (standard tools)

Optimality Verifier (Verification)

Mathematically verifies the proof that no cheaper plan exists

Model or implementation: VeriPB (Proof Checker)

Novel Architectural Elements

Integration of heuristic certificates directly into the proof stream
Use of reification variables to represent validity of heuristic estimates within the pseudo-Boolean logic

Modeling

Base Model: VeriPB (Proof System) / A* (Planning Algorithm)

Comparison to Prior Work

vs. Mugdan Approach 1: Avoids exponential increase in variables/actions by using PB constraints instead of pure SAT compilation
vs. Mugdan Approach 2: More general; supports backward-chaining heuristics (Pattern Databases) which Mugdan's approach struggles with
vs. Eriksson et al. (Unsolvability): Extends the concept from unsolvability to optimality (proving cost lower bounds)

Limitations

Generality of the proof system for *all* planning techniques remains a conjecture (though PDB and h^max are demonstrated)
Depends on the external VeriPB checker's performance
Overhead of proof logging is claimed to be 'modest' but specific scaling factors depend on the heuristic used

Reproducibility

The paper relies on the existing VeriPB proof checker. It discusses modifying the A* algorithm as a case study but the text does not provide a specific repository URL for the modified planner.

📊 Experiments & Results

Evaluation Setup

Case study on modifying A* search to produce proofs

Benchmarks:

Standard Planning Domains (implied) (Optimal Classical Planning)

Metrics:

Proof generation overhead
Verification time
Certificate size
Statistical methodology: Not explicitly reported in the paper

Main Takeaways

The paper presents a theoretical framework and a case study implementation.
Claims to demonstrate that A* can be modified to produce certificates with 'modest overhead'.
Claims to support any heuristic whose inferences can be expressed as pseudo-Boolean constraints.

📚 Prerequisite Knowledge

Prerequisites

Classical Planning (STRIPS formalism)
Propositional Logic and Satisfiability (SAT)
Proof Complexity (Cutting Planes)
Heuristic Search ($A^*$ algorithm)

Key Terms

STRIPS: A formal language for automated planning problems consisting of an initial state, goal states, and a set of actions with preconditions and effects.

Pseudo-Boolean (PB) constraint: A linear inequality over Boolean variables (e.g., $2x_1 + 3x_2 \ge 4$) capable of expressing arithmetic reasoning more compactly than standard SAT clauses.

Cutting Planes: A proof system for deriving linear inequalities, using rules like linear combination and division to prove unsatisfiability or bounds.

Reification: Representing the truth value of a constraint as a boolean variable (e.g., $r \Leftrightarrow C$), allowing the proof system to reason about the constraint itself.

RUP: Reverse Unit Propagation—an inference rule where a constraint is added if its negation leads to a conflict via unit propagation (standard in SAT proofs).

VeriPB: A formally verified proof checker tool that supports pseudo-Boolean proofs and cutting planes reasoning.

Heuristic Certificate: A proof construct that justifies why a specific heuristic estimate (lower bound on cost to goal) is valid (admissible) using PB constraints.

Pattern Database (PDB): A heuristic that stores pre-computed solution costs for simplified (abstracted) versions of the planning problem.

h^max: A heuristic that estimates cost by assuming sub-goals can be achieved independently and taking the maximum cost among them.