這幾天讀paper發現
2-SAT problem可以在多項式時間內被解出來，
由於
SAT和
3SAT是
NP-complete，很好奇為什麼2SAT例外呢？
就去網路上搜尋，很快的找到了英文的解答。
所謂的2SAT，就是可以寫成C1 and C2 and C3 ... and Cn, where C:clause，
且其size必須是2，例如一clause A∨B就是size為2的clause.
現在，我們定義一個directed graph G=(V,E)
V:對於每一個variable x，取x和~x兩個node
而
對於每一個clause A∨B，滿足A∨B，其實就是
滿足~A->B(若非A則B)或~B->A(若非B則A)，
E:對於每一個clause得到directed edge (~A,B)和(~B,A)
之後，把每一個(strongly)component依照
topoligically sort編號，而
strongly component內的編號皆編相同號碼。對於variable x，其編號函式為f(x)。
之後，由以下兩個Lemma，我們可以知道satisfying or not.
Lemma 1: formula F，假如有一個variable x，使得f(x)=f(~x)，則F是unsatisfiable.
證明：
由f(x)=f(~x)，知道x跟~x在同一strongly component，故存在一cycle:(x...~x...x)，
當我們嘗試x=true來滿足時，在其path:(x...~x)都必需為true，但~x不為true。(contradiction)
同理x=false時(~x=true)，也一樣是contradiction的情形。
Lemma 2: 假如對於在V上所有的x : f(x)!=f(~x)，則我們得到satisfying assignment經由設定
x=true if f(x)>f(~x)和x=false if f(x)<f(~x)
證明：
假定(assume)我們要得到矛盾的結果，
則在F中必定有一clause (A ∨B)是false，此時A和B皆為false。
By definition，f(A)<f(~A)和f(B)<f(~B)
而clause (A ∨B)貢獻兩條邊(~A,B)和(~B,A) to E，我們得到f(~A)<=f(B)和f(~B)<=f(A)，
結合以上，得到f(A) <f(~A)<=f(B)<f(~B) <=f(A)，矛盾。
至於演算法，
首先single pass F得到G的adjacency list，需O(n)。(n為clause數)
因此，這個graph有邊2n個和至多4n個的點。
對於每一個variable x，建一list L point到graph的x和~x.
而計算strongly component和那圖的topological order需O(n)
(至於是什麼方法，我也不清楚)，
之後，single pass L經由以上兩lemma的判斷，可知是否satisfying.
故The 2SAT problem for a formula F with n clauses can be solved in time O(n).
