基于伪布尔约束的经典规划伪布尔证明日志

我们引入一种用于经典规划任务的下界证书，可用于以独立第三方可验证的方式证明任务不可解或证明计划的最优性。我们描述了一个通用的基于伪布尔约束生成下界证书的框架，该框架对所使用的规划算法无关。作为一个案例研究，我们展示如何修改 $A^{*}$ 算法，以在代价适度增加的情况下产生最优性证明，这里我们以模式数据库启发式和 $h^\textit{max}$ 作为具体示例。相同的证明日志方法适用于任何其推理可有效表示为伪布尔约束推理的启发式方法。