UpMax: User partitioning for MaxSAT

要約

最大満足度 (MaxSAT) 問題のインスタンスは、ソフト句のセットをいくつかの素なセットに分割することによって効果的に解決できることが示されています。
分割方法は、文節の重み (階層化など) に基づいたり、数式のグラフ表現に基づいたりすることができます。
その後、最適なソリューションが見つかることを保証するためにマージ手順が適用されます。
この論文では、分割手順を MaxSAT 解決アルゴリズムから分離する UpMax と呼ばれる新しいフレームワークを提案します。
その結果、使用する MaxSAT アルゴリズムとは独立して、新しい分割手順を定義できます。
さらに、この分離により、新しい MaxSAT 式を構築するユーザーは、解決すべき問題の知識に基づいて分割スキームを提案することもできます。
いくつかの問題を使用してこのアプローチを説明し、分割が不満足度ベースの MaxSAT アルゴリズムのパフォーマンスに大きな影響を与えることを示します。

要約(オリジナル)

It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google