Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended algorithms and examples)

要約

私たちは、人間が理解できる方法で制約満足問題 (CSP) の解決策を段階的に説明するために最近提案された方法を構築します。
ここでの説明は、コスト関数を使用して単純性が定量化される一連の単純な推論ステップです。
説明生成のアルゴリズムは、派生した不満足式の最小不満足サブセット (MUS) の抽出に依存し、いわゆる非冗長説明と MUS 間の 1 対 1 対応を利用します。
ただし、MUS 抽出アルゴリズムは、特定のコスト関数に関してサブセットの最小性または最適性を保証しません。
したがって、私たちはこれらの形式的な基盤を構築し、改善の主な点、つまり、(特定のコスト指標に関して) 最適であると証明される説明を効率的に生成する方法に取り組みます。
そのために、私たちは、(1) 最適な制約付き不満足サブセットを見つけるためのヒット セット ベースのアルゴリズムを開発しました。
(2) 複数のアルゴリズム呼び出しにわたって関連情報を再利用する方法。
(3) ドメイン固有の情報を利用して説明シーケンスの生成を高速化する方法。
私たちは、多数の CSP 問題についてアルゴリズムを実験的に検証しました。
私たちのアルゴリズムは、説明の品質と計算時間の点で MUS アプローチよりも優れていることがわかりました (標準的な MUS アプローチよりも平均で最大 56 % 高速です)。

要約(オリジナル)

We build on a recently proposed method for stepwise explaining solutions of Constraint Satisfaction Problems (CSP) in a human-understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified using a cost function. The algorithms for explanation generation rely on extracting Minimal Unsatisfiable Subsets (MUS) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called non-redundant explanations and MUSs. However, MUS extraction algorithms do not provide any guarantee of subset minimality or optimality with respect to a given cost function. Therefore, we build on these formal foundations and tackle the main points of improvement, namely how to generate explanations efficiently that are provably optimal (with respect to the given cost metric). For that, we developed (1) a hitting set-based algorithm for finding the optimal constrained unsatisfiable subsets; (2) a method for re-using relevant information over multiple algorithm calls; and (3) methods exploiting domain-specific information to speed up the explanation sequence generation. We experimentally validated our algorithms on a large number of CSP problems. We found that our algorithms outperform the MUS approach in terms of explanation quality and computational time (on average up to 56 % faster than a standard MUS approach).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google