2-SAT
与えられた論理式を真にすることができるか判定する問題を充足可能性問題(SAT)という。特に、論理式を乗法標準形で表現したとき、ORでつながれた論理変数の個数が高々2であるものに対するSATを2-SATという。 各論理変数について真、偽に対応する頂点をつくる。このグラフ上に有向辺を張り、$ a \to bを辺$ (a,b)に対応させる。
このとき、ORを$ a \lor b \Leftrightarrow \lnot a \to b \land \lnot b \to aのように変形できることから論理式全体をIFで記述することができる。
強連結成分内の頂点はすべて真偽が一致しなければならないため、$ a, \lnot aが同じ強連結成分に含まれていた場合、論理式全体を真にすることは不可能であることがわかる。このような論理変数が存在しなければ必ず充足可能な真偽の割り当てが存在する。 OR:$ a \lor b \Leftrightarrow \lnot a \to b \land \lnot b \to a
NAND:$ \lnot (a \land b) \Leftrightarrow a \to \lnot b \land b \to \lnot a