Pseudo-Boolean Proof Logging for Optimal Classical Planning

要約

古典的な計画タスクの下限証明書を導入します。これは、独立した第三者が検証できる方法で、タスクの解決能力または計画の最適性を証明するために使用できます。
使用される計画アルゴリズムに不可知論される擬似ブールの制約に基づいて、下限証明書を生成するための一般的なフレームワークについて説明します。
ケーススタディとして、パターンデータベースヒューリスティックと$ h^\ textit {max} $を具体的な例として使用して、$ a^{*} $ algorithmを変更する方法を示します。
同じ証明ロギングアプローチは、推論が擬似ブールの制約に対する推論として効率的に表現できるヒューリスティックに対して機能します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google