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

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

假設 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\rightarrow \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\rightarrow \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 在這](https://github.com/klb3713/aoapc-book/blob/master/TrainingGuide/bookcodes/ch5/la3211.cpp)）。

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

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

第一眼看是 $O(VE)$ 第二眼看是 $O(V+E)$ 第三眼看是 $O(VE)$ ＝＝

大大們教ㄇ

## UPD：

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

## 註解
[原臉書網誌網址](https://www.facebook.com/notes/733860447199957/)，寫於2019年9月22日