arXiv:2504.18443v1 任务类型: 新颖 摘要: 我们引入了用于经典规划任务的下界证书，这些证书可以用来证明任务的不可解性或者计划的最优性，且这种证明可以通过第三方独立验证。我们描述了一种基于伪布尔约束生成下界证书的一般框架，这种框架对使用的规划算法持中立态度。 作为案例研究，我们展示了如何修改 $A^{*}$ 算法以产生具有良好开销的最优性证明，使用模式数据库启发式和 $h^\textit{max}$ 作为具体例子。相同的方法适用于任何其推断可以高效表达为伪布尔约束推理的启发式。