Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Pseudo-Boolean Proof Logging for Optimal Classical Planning

Dold, Simon ; Helmert, Malte ; Nordström, Jakob LU ; Röger, Gabriele and Schindler, Tanja (2025) 35th International Conference on Automated Planning and Scheduling, ICAPS 2025 35. p.54-63
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 hmax as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.

Please use this url to cite or link to this publication:
author
; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
Proceedings International Conference on Automated Planning and Scheduling, ICAPS
volume
35
edition
1
pages
10 pages
conference name
35th International Conference on Automated Planning and Scheduling, ICAPS 2025
conference location
Melbourne, Australia
conference dates
2025-11-09 - 2025-11-14
external identifiers
  • scopus:105017495382
DOI
10.1609/icaps.v35i1.36101
language
English
LU publication?
yes
id
2873bb74-5666-429c-9653-f05d9427155e
date added to LUP
2025-12-08 11:53:51
date last changed
2025-12-08 11:54:29
@inproceedings{2873bb74-5666-429c-9653-f05d9427155e,
  abstract     = {{<p>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<sup>∗</sup> algorithm to produce proofs of optimality with modest overhead, using pattern database heuristics and h<sup>max</sup> as concrete examples. The same proof logging approach works for any heuristic whose inferences can be efficiently expressed as reasoning over pseudo-Boolean constraints.</p>}},
  author       = {{Dold, Simon and Helmert, Malte and Nordström, Jakob and Röger, Gabriele and Schindler, Tanja}},
  booktitle    = {{Proceedings International Conference on Automated Planning and Scheduling, ICAPS}},
  language     = {{eng}},
  pages        = {{54--63}},
  title        = {{Pseudo-Boolean Proof Logging for Optimal Classical Planning}},
  url          = {{http://dx.doi.org/10.1609/icaps.v35i1.36101}},
  doi          = {{10.1609/icaps.v35i1.36101}},
  volume       = {{35}},
  year         = {{2025}},
}