Empirical Evaluation of the Implicit Hitting Set Approach for Weighted CSPs

要約

SAT テクノロジーは、さまざまな分野で驚くほど効果的であることが証明されています。
ただし、加重 CSP 問題に関しては、専用のアルゴリズムが常に優れています。
これまで十分に研究されていないアプローチの 1 つは、SAT を Implicit Hitting Set アプローチと組み合わせて使用​​することです。
この研究では、既存の参照アルゴリズムに代わるいくつかの方法を検討します。
代替案は主に関連するブール フレームワークから借用したもので、IHS アプローチの 2 つの主要なコンポーネント、つまり低コストのヒット ベクトルの計算と、それらの高コスト コアへの変換のトレードオフを考慮します。
それぞれについて、4 つの強度レベルを提案します。
コスト関数の結合の有用性もテストするため、実験では 32 の異なる実装を考慮します。
私たちの実証研究によると、WCSP にとって最適な代替案を特定するのは簡単ではありません。
それにもかかわらず、コスト関数をマージしてエンコードし、最大のコアを抽出することは、堅牢なアプローチであると思われます。

要約(オリジナル)

SAT technology has proven to be surprisingly effective in a large variety of domains. However, for the Weighted CSP problem dedicated algorithms have always been superior. One approach not well-studied so far is the use of SAT in conjunction with the Implicit Hitting Set approach. In this work, we explore some alternatives to the existing algorithm of reference. The alternatives, mostly borrowed from related boolean frameworks, consider trade-offs for the two main components of the IHS approach: the computation of low-cost hitting vectors, and their transformation into high-cost cores. For each one, we propose 4 levels of intensity. Since we also test the usefulness of cost function merging, our experiments consider 32 different implementations. Our empirical study shows that for WCSP it is not easy to identify the best alternative. Nevertheless, the cost-function merging encoding and extracting maximal cores seems to be a robust approach.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google