2-SAT 簡易求解法與正確性證明

此文由來

小時候看劉汝佳的訓練指南裡面 2-SAT 求解，做完 SCC 還要 for loop dfs，看起來很麻煩，後來看 E-Maxx Algorithms 裡的 2-SAT 教學才發現有很簡單的求解法，可是我比較笨，他的證明一直看不太懂，今天在校草級高顏值大肌肌學霸林庭風推薦的優質程式討論區「Taiwan 程式語言讀書會」裡看到有人在問上面那種構造法的正確性，我認真想了一小時多終於會證了。（討論區文章連結）

以下節錄自我的回文（之後可能會把它修好一點）：

假設 2-SAT 做完強連通分解並把 SCC 依拓樸順序由小到大編號
那麼下面的演算法為什麼能構出一組解

for v = 1 to n:
    if SCC_ID[v] == SCC_ID[~v]:
        return NO ANSWER
    if SCC_ID[v] < SCC_ID[~v]:
        ans[v] = 0
    else:
        ans[v] = 1

(1)

已知對於所有的變數

$v$，

$v$ 跟

$\sim v$ 不在同一個 SCC 裡。
當你要輸出一組解，且

$\sim a$ 的索引在

$a$ 之前時，

$a$ 一定走不到

$\sim a$。

(proof)assume for contradiction that a can reach ~a.

1. if ~a can reach a, then a and ~a belong to the same SCC, -><-
2. if ~a can't reach a, then the topological order of a is before ~a, -><-

(2)

以下 x->y 表示 x can reach y
假設你選了 a ，存不存在 b s.t. a->b and a->~b ?
(proof) 不存在
assume for contradiction that b exists
因為 2-SAT 加邊是有對稱性的
(x,~y) 跟 (~y,x) 會同時被加進去
因此，
a->b implies

$\sim b\to \sim a$
a->~b implies b->~a
所以 a->~a，矛盾

到這邊證明了，這樣的挑法挑到的點往下走都不會無解

(3)

令 V 表示所有點， S 表示我們挑的點集
若 a in S & a->b & b not in S ，可是選 a imply b，所以 S 就不是一組解

所以我們還需要證明
for all a in S, for all b in V
if a->b then b in S
因為 S 中一定恰有 b 或 ~b 其中一點(by 我們的挑法)
所以
assume for contradiction that a in S and a->b and ~b in S
我們選了 a 表示 SCC_ID[a] > SCC_ID[~a]
a->b 表示 SCC_ID[a] <= SCC_ID[b]
選 ~b 不選 b 表示 SCC_ID[b] < SCC_ID[~b]
a->b implies

$\sim b\to \sim a$ 也就是 SCC_ID[~b] <= SCC_ID[~a]

put them together,
SCC_ID[~b] <= SCC_ID[~a] < SCC_ID[a] <= SCC_ID[b] < SCC_ID[~b]

表示 SCC_ID[~b] < SCC_ID[~b]，矛盾
所以我們挑出來的是對的
到這邊才算證明完畢

延伸討論

其實上面的做法正確性仰賴 2-SAT 加邊時的對稱性，如果今天問題是：

有

$n$ 個 Boolean 變數

$a_1,a_2,\cdots ,a_n$，給你

$m$ 條邊，每條是

$(a_i=x)$ 這個節點到

$(a_j=y)$ 節點的有向邊，求一組解

那圖中節點間的邊就可以任意連，沒有對稱性，應該還是需要用劉汝佳那個先填 0，發現矛盾再回溯重新填 1 的演算法（code 在這）。

此外，他的演算法還能做到找最小字典序的解之類的，這邊的做不到。

可是我不太確定他的演算法的時間複雜度＝＝

第一眼看是

$O(VE)$ 第二眼看是

$O(V+E)$ 第三眼看是

$O(VE)$ ＝＝

大大們教ㄇ

UPD：

其實，加了一條 a=x -> b=y 的邊後，如果選了 b=~y 又選 a=x 就會無解，所以加上 b=~y -> a=~x 的邊也是好的。所以 bool 變數 imply 關係的圖一定會有對稱性，延伸討論中我說「任意連邊就沒有對稱性因此不能用文中的演算法」是錯的，只要自己加上對稱的邊即可。

註解

原臉書網誌網址，寫於2019年9月22日