2-SATを解いた時のメモ

Algorithm

2-SATとは

SATとはsatisfiability(充足性)の略で、与えられた論理式を満たす真偽値の組合せが存在することをいう。

特に2-SATとは、変数がx_1からx_nまであるとして以下の形の論理式について変数の真偽値の組合せを考える問題である。

(y_1 \vee y_2) \wedge (y_3 \vee y_4) \wedge ... \wedge (y_{2m-1} \vee y_{2m})
ここで
y_i \in \{x_1, x_2, ... , x_n, \bar{x_1}, \bar{x_2}, ... , \bar{x_n}\}

論理積でつながれたひとつひとつの部分(節)に変数が二つある(節の長さが2である)ので2-SATという。

2-SATの解法について

2-SATに対しては、節の数と変数の数に対する線形時間のアルゴリズムが存在する。ちなみに節の長さが3以上の場合この問題はNP完全に属する。

2-SATを解くにはImplication graphというグラフを構築する必要がある。次節でこのグラフについて述べる。

Implication graphの構築

Implication

Implicationとは「包含」という意味であり、論理で言えば論理包含がこれにあたる。命題P, Qに対しての論理包含を P ⇒ Q 等と書き、「Pが偽またはQが真」という意味を表す。

P ⇒ Q は 「Pが偽またはQは真」ということから論理包含と論理和の関係がわかる。

(\bar{P} \Rightarrow Q) \Leftrightarrow (P \vee Q)

同様にして Q ⇒ P についても

(\bar{Q} \Rightarrow P) \Leftrightarrow (Q \vee P)

である。

(\bar{P} \Rightarrow Q) \Leftrightarrow (P \vee Q) \Leftrightarrow (Q \vee P) \Leftrightarrow (\bar{Q} \Rightarrow P)

ということに注目すると

(P \vee Q) \Leftrightarrow (\bar{P} \Rightarrow Q) \wedge (\bar{Q} \Rightarrow P)

であると言える。これによって入力の論理式の論理和を全て論理包含によって書きなおせる。

グラフの構築

次にImplication graphを構築する。このグラフは名の通り、論理包含の関係を表現したものである。

このグラフを G = (V, E) と置くと、頂点集合Vは変数とその否定を表し、辺集合Eは論理包含の関係を表す。

V = \{x_1, x_2, ... , x_n, \bar{x_1}, \bar{x_2}, ... , \bar{x_n}\}
E = \{(u, v) | u, v \in V, u \Rightarrow v \}

つまり u ⇒ v の場合にだけ頂点u, v間に有向辺が存在する。

グラフの性質

このグラフの部分頂点集合である強連結成分について考える。強連結成分であるということはその集合内の任意の2頂点間に有向道が存在するということである。

Implication graphにおいて、ある頂点xからyへの有向道を考える。xからyには、その間にある頂点をいくつか(0個かもしれない)たどって行くことができる。たとえばこの時x, y間にある頂点が2つあったとして、その2つをa, bと置いてみると以下のような関係があるのは明らかである。

x \Rightarrow a
a \Rightarrow b
b \Rightarrow y

三段論法 (P ⇒ Q) ∧ (Q ⇒ R) ⇒ (P ⇒ R) を用いれば、以下の関係が分かる。

x \Rightarrow y

つまり、xからyへの有向道が存在するということは x ⇒ y ということである。

さらに、強連結成分の定義からyからxへの有向道も存在する。よって y ⇒ x ということも言える。

このことから x ⇔ y、つまりある強連結成分に属する頂点が示す変数の真偽値は全て等しいということが分かる。

Implication graphの利用

先ほど確認した同値関係を使って2-SATが解ける。

与えられた論理式を満たす組合せがないということは、変数の真偽値の関係に矛盾が生じているということで、この矛盾とは「ある変数の真偽値と、その否定の真偽値が一致する」ということである。

真偽値が一致するかどうかを調べるには先に言ったように強連結成分を見ればよい。

つまり、Implication graphを強連結成分分解した結果、ある変数とその否定が同じ強連結成分に属していた場合、与えられた論理式は充足できないということになる。

最後に

この文章はJAPLJが英語版Wikipediaを読み、それを用いて実際に2-SATを解いたときに学んだことのメモです。

英語の読み違いや知識不足などで誤りが含まれている可能性があります。何か誤りを見つけた場合は教えてください。