2SAT

強連結成分分解のアルゴリズムをゼミでやったのでメモ。
2SATは強連結成分分解を利用して解ける。

2SATは多項式時間で解ける。ちなみに3SATはNP完全。解き方は２つある。
(1)ある変数xの割り当てを0で固定すると、2SATなので、xを含む節のxとは異なる変数の割り当てが決まる。
このようにして矛盾が起こると、xへの割り当てが決定し、xを含む節を消去して再帰。
(2)2SATなので節は(x∨¬y)のような形をしている。これはy⇒xと同じである
各論理変数、論理否定それぞれに頂点を用意して、y⇒xを式が含んでいれば有効辺(y,x)をグラフに加える。
このようにしてできたグラフに強連結成分分解アルゴリズムを適用し、ある強連結成分が同じ変数の真リテラルと偽リテラルを含んだときに充足割り当てが存在しなくなる。