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