arXiv:2504.18443v2 宣告类型:替换 摘要:我们引入了用于经典规划任务的下界证书，这些证书可以用于证明任务的不可解性或计划的最优性，并且第三方可以验证这些证明。我们描述了一个基于伪布尔约束生成下界证书的一般框架，该框架与使用的规划算法无关。 作为案例研究，我们展示了如何通过修改 \(A^*\) 算法并使用模式数据库启发式和 \(h^{\text{max}}\) 等具体示例来生成具有适度开销的最优性证明。相同的方法对所有可以通过高效表达为伪布尔约束推理的启发式方法都适用。