为经典规划提供可验证的最优性证明，让结果可信且无需依赖原始算法。
Pseudo-Boolean Proof Logging for Optimal Classical Planning
- 用伪布尔约束构建规划问题的下界证书，与具体算法无关。
- 在A*算法中加入小开销即可生成最优性证明，支持模式数据库和h_max启发式。
- 适合需要严格验证规划结果的场景，如安全关键系统或学术验证。
我们提出经典规划任务的下界证书，可用于独立第三方验证任务不可解性或计划最优性。设计了一个基于伪布尔约束的通用证书生成框架，对所用规划算法无依赖性。以A*算法为例，展示了如何通过引入模式数据库启发式和h^max，以较小额外开销生成最优性证明。该方法适用于所有其推理可高效表示为伪布尔约束的启发式。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。