On Exploiting Hitting Sets for Model Reconciliation

要約

人間を意識した計画では、計画エージェントは人間のユーザーに、その計画が最適である理由を説明する必要がある場合があります。
これを行うための一般的なアプローチはモデル調整と呼ばれ、エージェントは自分のモデルと人間のモデルの違いを調整して、計画が人間のモデルでも最適になるように試みます。
このホワイトペーパーでは、計画の領域を超えて拡張されるモデル調整のためのロジックベースのフレームワークを紹介します。
より具体的には、数式 $\varphi$ を伴う知識ベース $KB_1$ とそれを伴わない 2 番目の知識ベース $KB_2$ が与えられた場合、モデル調整は $KB_1$ のカーディナリティ最小サブセットの形式で説明を求めます。
$KB_2$ に統合すると含意が可能になります。
私たちのアプローチは、矛盾の分析の文脈から生まれたアイデアに基づいており、適切な説明を特定するために、最小修正セット (MCS) と最小不満足セット (MUS) の間の既存のヒット セットの双対性を利用します。
ただし、単一の知識ベースを前提とした一貫性のない式を対象とした研究とは異なり、MCS と MUS は 2 つの異なる知識ベースで計算されます。
この論文の最後は、プランニング インスタンスに対して新しく導入されたアプローチの実証的評価であり、既存の最先端のソルバーや、他のソルバーでは対応できなかった最近の SAT コンテストの一般的な非プランニング インスタンスよりも優れたパフォーマンスを示すことを示しています。
存在します。

要約(オリジナル)

In human-aware planning, a planning agent may need to provide an explanation to a human user on why its plan is optimal. A popular approach to do this is called model reconciliation, where the agent tries to reconcile the differences in its model and the human’s model such that the plan is also optimal in the human’s model. In this paper, we present a logic-based framework for model reconciliation that extends beyond the realm of planning. More specifically, given a knowledge base $KB_1$ entailing a formula $\varphi$ and a second knowledge base $KB_2$ not entailing it, model reconciliation seeks an explanation, in the form of a cardinality-minimal subset of $KB_1$, whose integration into $KB_2$ makes the entailment possible. Our approach, based on ideas originating in the context of analysis of inconsistencies, exploits the existing hitting set duality between minimal correction sets (MCSes) and minimal unsatisfiable sets (MUSes) in order to identify an appropriate explanation. However, differently from those works targeting inconsistent formulas, which assume a single knowledge base, MCSes and MUSes are computed over two distinct knowledge bases. We conclude our paper with an empirical evaluation of the newly introduced approach on planning instances, where we show how it outperforms an existing state-of-the-art solver, and generic non-planning instances from recent SAT competitions, for which no other solver exists.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google