2-SAT (多項式時間で解ける)

**2-SAT (多項式時間で解ける)**は、各節が高々2個のリテラルからなるCNFの充足可能性問題である。

仕組み

各変数xについてxと¬xを頂点にし、節(a∨b)を含意¬a→bと¬b→aへ変換する。含意グラフの強連結成分でxと¬xが同一成分なら充足不能である。

強連結成分はO(V+E)で求まり、節数に対して線形時間で判定できる。

(x∨y)∧(¬x∨y)では、含意をたどって矛盾しない真理値を復元できる。

一般の3-SATまで同じ方法で多項式時間になるわけではない。