2-SAT のアルゴリズムの証明

概要

蟻本で 2-SAT のアルゴリズムを最初に見たとき、私はその正当性について何ら疑問を抱きませんでした。これは私の頭がよく回ったからではなく、単に行間に気づいていなかったからということに最近気づきましたので、反省を兼ねて記録します。

反例のようなもの (反例ではない)

まず $x \lor y \Leftrightarrow (\lnot x \Rightarrow y) \land (\lnot y \Rightarrow x)$ に辺を張る部分を考えます。そもそも $x \lor y \Leftrightarrow (\lnot x \Rightarrow y)$ であり、 $\lnot x \rightarrow y$ へ辺を張るだけで十分なように思われます。 (これがまずい理由がわかる方はこの記事を読む意味がありません、申し訳ありません)

$x \lor y$ のみからなる 2-SAT のグラフを書いてみます。 $\lnot x \rightarrow y$ だけに辺を張ると、例えば以下のような順序のトポロジカルソートが考えられます。

$x,y$ の真偽を決めてみます。 $x \lt \lnot x$ なので $x = 0$ であり、同様に $y = 0$ となります。ところがこの割り当ては $x \lor y$ を満たしていません。これは「 $x$ から $\lnot x$ に到達可能なら $x = 0$ 」が必要条件であって、十分条件ではないことに起因しています。トポロジカルソートを一つ選んだ時対応する割り当てが定まることから、その割り当てが全体で整合することは (直ちには) 導かれません。
一方で $\lnot y \Rightarrow x$ にも辺を張るとこのようなことは発生しません。裏を返せば 2-SAT の正統性の証明は、明示的あるいは暗黙的に「 $x \rightarrow y$ の辺があるなら $\lnot y \rightarrow \lnot x$ の辺がある」事実を使用していることになります。

証明

トポロジカルソートして大小で真偽を割り当てたとき、それが全体で整合することを示します。

不整合を仮定すると、 $x = 1 \land y = 0$ なる $x,y$ であって $x \rightarrow y$ の辺を持つものが存在します。このとき $x \le y$ です。また、 $x,y$ の真偽の割り当てから $\lnot x \lt x$ 及び $y \lt \lnot y$ が分かります。ここで $x \rightarrow y$ より $\lnot y \rightarrow \lnot x$ の辺が存在しますが、 $\lnot x \lt x \le y \lt \lnot y$ と矛盾します。

よって割り当ては整合します。