最大満足問題

計算複雑性理論において、最大充足可能性問題( MAX-SAT ) は、与えられたブール式の連言標準形において、式の変数に真理値を割り当てることによって真にできる節の最大数を決定する問題である。これは、すべての節を真にする真理値割り当てが存在するかどうかを問う ブール充足可能性問題の一般化である。

連言標準形式

${\displaystyle (x_{0}\lor x_{1})\land (x_{0}\lor \lnot x_{1})\land (\lnot x_{0}\lor x_{1})\land (\lnot x_{0}\lor \lnot x_{1})}$

は満足できません。2 つの変数にどの真理値が割り当てられても、4 つの節のうち少なくとも 1 つは偽になります。ただし、4 つの節のうち 3 つが真になるように真理値を割り当てることは可能です。実際、すべての真理値割り当てでこのようになります。したがって、この式が MAX-SAT 問題のインスタンスとして与えられた場合、問題の解は 3 になります。

MAX-SAT問題はOptP完全^[1]であり、したがってNP困難である。なぜならその解はNP完全であるブール充足可能性問題の解に簡単につながるからである。

最適解の保証された近似率内でいくつかの節を満たす問題の近似解を見つけることも困難です。より正確には、この問題はAPX完全であり、したがってP = NPでない限り多項式時間近似スキームを許容しません。^{[2] [3] [4]}

より一般的には、重み付きバージョンの MAX-SAT を次のように定義できます。各節に非負の重みが割り当てられた連言正規形式が与えられた場合、満たされる節の合計重みを最大化する変数の真理値を見つけます。MAX-SAT 問題は、すべての重みが 1 である重み付き MAX-SAT の例です。^{[5] [6] [7]}

各変数を確率1/2で真になるようにランダムに割り当てると、期待される 2近似値が得られます。より正確には、各節に少なくともk個の変数がある場合、これは(1 − 2 ^{− k} )近似値をもたらします。^{[8]このアルゴリズムは、}条件付き確率法を使用してランダム化を解除できます。^[9]

MAX-SAT は、整数線形計画法(ILP)を使用して表現することもできます。連言正規形式F を変数x ₁、x ₂、...、x _nで固定し、CでFの節を表します。 Cの各節cについて、S ⁺ _cとS ⁻ _cで、それぞれcで否定されない変数の集合とcで否定される変数の集合を表します。 ILP の変数y _{x は}式Fの変数に対応し、変数z _{c は}節に対応します。 ILP は次のとおりです。

上記のプログラムは、次の線形プログラムLに緩和できます。

この緩和法を用いた次のアルゴリズムは、期待される(1-1/ e )近似である: ^[10]

1. 線形計画Lを解いて解Oを得る
2. 変数x が確率y _xで真になるように設定します。ここでy _{x は}Oで指定された値です。

このアルゴリズムは、条件付き確率法を使用して非ランダム化することもできます。

1/2 近似アルゴリズムは節が大きい場合に有効ですが、(1-1/ e ) 近似は節が小さい場合に有効です。これらは次のように組み合わせることができます。

1. （ランダム化されていない）1/2近似アルゴリズムを実行して、真理値割り当てX を取得します。
2. (ランダム化されていない)(1-1/e)近似を実行して、真理値の割り当てYを取得します。
3. 満たされる節の重みを最大化するXまたはYのいずれかを出力します。

これは決定論的因子（3/4）近似である。^[11]

公式について

$${\displaystyle F=\underbrace {(x\lor y)} _{{\text{weight }}1}\land \underbrace {(x\lor \lnot y)} _{{\text{weight }}1}\land \underbrace {(\lnot x\lor z)} _{{\text{weight }}2+\epsilon }}$$

ここで、(1-1/ e )近似は各変数を確率1/2でTrueに設定するため、1/2近似と同じように動作します。ランダム化解除中にxの割り当てが最初に選択されると仮定すると、ランダム化解除アルゴリズムは総重みが の解を選択しますが、最適解は重みが です。^[12]${\displaystyle \epsilon >0}$${\displaystyle 3+\epsilon }$${\displaystyle 4+\epsilon }$

最先端のアルゴリズムはAvidor、Berkovitch、Zwickによるもので^{[13] [14]}、その近似率は0.7968です。彼らはまた、近似率が0.8353と推測される別のアルゴリズムも提供しています。

近年、MAX-SAT の正確なソルバーが数多く開発されており、その多くはブール充足可能性問題と関連問題に関する有名な会議である SAT カンファレンスで発表されました。2006 年に SAT カンファレンスは、疑似ブール充足可能性問題や量化ブール式問題で過去に行われたように、MAX-SAT の実用的なソルバーのパフォーマンスを比較する最初の MAX-SAT 評価を主催しました。NP困難性のため、大規模な MAX-SAT インスタンスは一般に正確に解くことができず、近似アルゴリズム やヒューリスティックに頼らざるを得ないことがよくあります^[15]

最新の Max-SAT 評価に提出されたソルバーがいくつかあります。

• 分岐限定法ベース: Clone、MaxSatz ( Satzベース)、IncMaxSatz、IUT_MaxSatz、WBO、GIDSHSat。
• 満足度ベース: SAT4J、QMaxSat。
• 不満足性ベース: msuncore、WPM1、PM2。

MAX-SAT は、ブール充足可能性問題の最適化拡張の 1 つです。ブール充足可能性問題は、与えられたブール式の変数を、式が TRUE と評価されるように割り当てることができるかどうかを判断する問題です。2-充足可能性のように、節が最大 2 つのリテラルに制限されている場合は、MAX-2SAT問題になります。3-充足可能性のように、節ごとに最大 3 つのリテラルに制限されている場合は、 MAX-3SAT問題になります。

連言標準形ブール式の充足可能性に関連する問題は数多くあります。

• 意思決定の問題:
  • 2SAT
  • 3SAT
• 満たされる節の数を最大化することを目的とする最適化問題:
  • MAX-SATおよび対応する加重バージョン加重MAX-SAT
  • MAX- k SAT、各節にはちょうどk 個の変数があります。
    • マックス2SAT
    • マックス3SAT
    • マックスエクサット
  • 部分的最大充足可能性問題 (PMAX-SAT) は、特定の節のサブセットの任意の割り当てによって充足できる節の最大数を尋ねます。残りの節は充足される必要があります。
  • ソフトSAT問題とは、SAT問題のセットが与えられたときに、任意の割り当てによって満たすことができる問題の最大数を問う問題である。^[16]
  • 最小満足可能性問題。
• MAX-SAT問題は、制約充足問題の変数が実数の集合に属する場合に拡張することができる。この問題は、制約のq緩和交差が空にならないような最小のqを見つけることである。 ^[17]

• ブール充足可能性問題
• 制約の充足
• 理論による充足可能性

• http://www.satisfiability.org/
• https://web.archive.org/web/20060324162911/http://www.iiia.csic.es/~maxsat06/
• http://www.maxsat.udl.cat
• 隠れた最適解を備えた加重 Max-2-SAT ベンチマーク
• MAX-SAT近似に関する講義ノート

• Vazirani、Vijay V. (2001)、近似アルゴリズム(PDF)、Springer-Verlag、ISBN 978-3-540-65367-7