Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers

要約

MaxSAT は、有名な NP 完全充足可能性問題 (SAT) の最適化バージョンです。
MaxSAT のアルゴリズムには、主に完全ソルバーとローカル検索不完全ソルバーが含まれます。
多くの完全なソルバーでは、より良い解決策が見つかると、ソフト競合擬似ブール (SPB) 制約が生成され、アルゴリズムがより良い解決策を見つけるように強制されます。
多くのローカル検索アルゴリズムでは、文節の重み付けは検索方向を効果的に導くための重要な手法です。
この論文では、SPB 制約を局所検索法の文節重み付けシステムに移し、アルゴリズムをより良い解決策に導くことを提案します。
さらに、定数値を使用して文節の重みを調整するという伝統を打ち破る、適応的な文節の重み付け戦略を提案します。
上記の方法に基づいて、我々は、MaxSAT ローカル検索ソルバーの文節重み付けに新しい観点を提供する SPB-MaxSAT と呼ばれる新しいローカル検索アルゴリズムを提案します。
広範な実験により、提案された方法の優れたパフォーマンスが実証されています。

要約(オリジナル)

MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT). Algorithms for MaxSAT mainly include complete solvers and local search incomplete solvers. In many complete solvers, once a better solution is found, a Soft conflict Pseudo Boolean (SPB) constraint will be generated to enforce the algorithm to find better solutions. In many local search algorithms, clause weighting is a key technique for effectively guiding the search directions. In this paper, we propose to transfer the SPB constraint into the clause weighting system of the local search method, leading the algorithm to better solutions. We further propose an adaptive clause weighting strategy that breaks the tradition of using constant values to adjust clause weights. Based on the above methods, we propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers. Extensive experiments demonstrate the excellent performance of the proposed methods.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google