An Efficient Algorithm for Solving the 2-MAXSAT Problem

技術要約：2-MAXSAT問題を解くための効率的なアルゴリズム

問題の定義
本論文は、最大充足可能性（MAXSAT）問題の制限されたバージョンである2-MAXSAT問題を取り扱う。$m$個のブール変数$V$の集合と、標準連言形式（CNF）における$n$個の節$C$のコレクションが与えられたとき、各節は高々2つのリテラルを含む。目的は、充足される節の数を最大化する真理値割り当てを見つけることである。この制限下においても、本問題がNP完全であることは確立されている。

手法
提案されているアルゴリズムは、従来の分枝限定法や近似法とは異り、問題を選言標準形（DNF）の最大化タスクへと変換し、特殊なグラフベースの探索構造を利用する。この手法は、主に以下の3つの段階で進行する。

1. DNFへの変換:
   アルゴリズムは、元のCNF式$C$から新しいDNF式$D$を構築する。$C$におけるすべての節 $C_i = l_{i1} \lor l_{i2}$ に対して、アルゴリズムは新しい補助変数 $x_i$ を導入し、2つの連言 $D_{i1} = l_{i1} \land x_i$ および $D_{i2} = l_{i2} \land \neg x_i$ を生成する。結果として得られる式$D$は、$2n$個の連言で構成される。論文内の命題1は、$V \cup \{x_1, \dots, x_n\}$ に対する真理値割り当ての下で、$C$が少なくとも$n^*$個の充足可能な節を持つことは、$D$が少なくとも$n^*$個の充足可能な連言を持つことと同値であることを確立している。

2. グラフ表現（p-グラフとトライ）:*
   $D$における連言を充足する真理値割り当てを効率的に表現するために、本論文ではp-グラフ*を導入している。

   • 変数シーケンス: 各連言は、変数の出現頻度に基づくソートされた変数シーケンスに変換される。負のリテラルは、変数 $c$ が真または偽（あるいはスキップ可能）であっても連言の真偽に影響を与えないことを表す特別な表記 $(c, *)$ を用いて処理される。
   • p-グラフ: 連言における単一の変数シーケンスを表す有向グラフであり、ノードはシーケンス内の変数に対応する。 「スパン（Spans）」（変数をスキップするエッジ）は $(c, *)$ の選択肢を表す。
   • p-グラフ:* p-グラフを洗練させたものであり、「重複スパン（overlapped spans）」（連続するオプション変数）を推移的閉包によってマージしたものである。これにより、グラフが特定の連言に対するすべての有効な真理値割り当てを正しく表現することが保証される。
   • トライのような構造 ($G$): すべてのp*-グラフは、単一のトライのようなグラフ $G$ に統合される。この構造は、冗長なチェックを避けるために共通の変数シーケンスをクラスター化する。グラフには、パスが分岐する「分岐ノード」が含まれる。

3. 再帰的なボトムアップ探索:
   コアとなるアルゴルズムである SEARCH(G) は、充足可能な連言の最大部分集合を見つけるために、グラフ $G$ をボトムアップ（後順走査）方式で探索する。

   • 到達可能部分集合 (RS): 分岐ノード $v$ に対して、アルゴリズムは、祖先からのスパンを介して到達可能なノードの「到達可能部分集合」を計算する。これらの部分集合は、特定の変数をバイパスすることによって同時に充足できる連言のグループを表す。
   • 上界 (upBounds): RSに基づき、アルゴリズムは部分グラフのマージを可能にするノードの集合である「上界（upper boundaries）」を特定する。
   • 再帰的構築: 分岐ノードに遭遇した際、アルゴリズムは上界にあるノードを根とする、より小さく新しいトライのような部分グラフを構築する。接続性を維持するために、仮想的なルート（元の分岐ノード）が追加される。アルゴリズムは、これらの部分グラフに対して SEARCH を再帰的に呼び出す。
   • 最適化: 冗長な計算を防ぐため、アルゴリズムは2つの改善策を採用している。(1) RSの計算を現在の分岐ノードとその最も近い祖先分岐ノードの間のセグメントに限定すること、および (2) ハッシュ配列を使用して、以前に訪問した部分グラフの結果をキャッシュし、繰り返しの再帰呼び出しを抑制することである。

主な貢献

• 変換技術: 2-MAXSAT問題を、DNFにおける最大充足連言問題への多項式時間での還元。
• p-グラフ構造:* オプション変数を含む連言の真理値割り当てを正確かつコンパクトに表現するための、p*-グラフの定義とその推移的閉包。
• 再帰的トライ探索: 「到達可能部分集合」と「上界」を利用して解空間を効率的にマージしながら、トライのようなグラフ構造を動的に構築・探索する新しい再帰アルゴリズム。
• 複雑性分析: 本論文は、アルゴリズムが多項式時間の範囲内で動作するという詳細な分析を提供している。

結果と複雑性
本論文は、提案されたアルゴリズムの最悪時間計算量が、節の数を $n$、変数の数を $m$ とすると $O(n^2 m^4)$ に抑えられると断言している。

• 初期のトライおよびp*-グラフの構築には $O(nm^2)$ かかる。
• 再帰的探索には、高々 $O(nm)$ 個の分岐ノードが含まれる。
• 各ステップでのグラフの高さの減少により、各分岐ノードは最大 $O(m)$ 回の再帰呼び出しに関与する。
• 呼び出しごとの部分グラフ構築のコストは $O(nm^2)$ である。
• これらの要因を組み合わせることで、$O(n^2 m^4)$ の境界が得られる。

意義と主張
本論文は、2-MAXSAT問題がNP完全であることが知られているため、これを解くための多項式時間アルゴリズムの存在は、P = NP の証明を構成すると結論付けている。著者らは、この結果が P = NP の証明を提供し、充足可能性問題に関する計算複雑性の理解を根本的に変えるものであると述べている。本研究は、NSERC（カナダ）の支援を受けた、会議論文の修正および拡張として提示されている。