原文地址：http://www.cppblog.com/MatoNo1/archive/2011/07/13/150766.aspx
【2-SAT問題】
現有一個由N個布爾值組成的序列A，給出一些限制關系，比如A[x] AND A[y]=0、A[x] OR A[y] OR A[z]=1等，要確定A[0..N-1]的值，使得其滿足所有限制關系。這個稱為SAT問題，特別的，若每種限制關系中最多只對兩個元素進行限制，則稱 為2-SAT問題。
由於在2-SAT問題中，最多只對兩個元素進行限制，所以可能的限制關系共有11種：
A[x]
NOT A[x]
A[x] AND A[y]
A[x] AND NOT A[y]
A[x] OR A[y]
A[x] OR NOT A[y]
NOT (A[x] AND A[y])
NOT (A[x] OR A[y])
A[x] XOR A[y]
NOT (A[x] XOR A[y])
A[x] XOR NOT A[y]
進 一步，A[x] AND A[y]相當於(A[x]) AND (A[y])（也就是可以拆分成A[x]與A[y]兩個限制關系），NOT(A[x] OR A[y])相當於NOT A[x] AND NOT A[y]（也就是可以拆分成NOT A[x]與NOT A[y]兩個限制關系）。因此，可能的限制關系最多只有9種。
在實際問題中，2-SAT問題在大多數時候表現成以下形式：有N對物品，每 對物品中必須選取一個，也只能選取一個，並且它們之間存在某些限制關系（如某兩個物品不能都選，某兩個物品不能都不選，某兩個物品必須且只能選一個，某個 物品必選）等，這時，可以將每對物品當成一個布爾值（選取第一個物品相當於0，選取第二個相當於1），如果所有的限制關系最多只對兩個物品進行限制，則它 們都可以轉化成9種基本限制關系，從而轉化為2-SAT模型。
【建模】
其實2-SAT問題的建模是和實際問題非常相似的。
建 立一個2N階的有向圖，其中的點分為N對，每對點表示布爾序列A的一個元素的0、1取值（以下將代表A[i]的0取值的點稱為i，代表A[i]的1取值的 點稱為i'）。顯然每對點必須且只能選取一個。然后，圖中的邊具有特定含義。若圖中存在邊<i, j>，則表示若選了i必須選j。可以發現，上面的9種限制關系中，后7種二元限制關系都可以用連邊實現，比如NOT(A[x] AND A[y])需要連兩條邊<x, y'>和<y, x'>，A[x] OR A[y]需要連兩條邊<x', y>和<y', x>。而前兩種一元關系，對於A[x]（即x必選），可以通過連邊<x', x>來實現，而NOT A[x]（即x不能選），可以通過連邊<x, x'>來實現。
【O(NM)算法：求字典序最小的解】
根據2-SAT建成的圖中邊的定義可以發現，若圖中i到j有路徑，則若i選，則j也要選；或者說，若j不選，則i也不能選；
因此得到一個很直觀的算法：
（1）給每個點設置一個狀態V，V=0表示未確定，V=1表示確定選取，V=2表示確定不選取。稱一個點是已確定的當且僅當其V值非0。設立兩個隊列Q1和Q2，分別存放本次嘗試選取的點的編號和嘗試不選的點的編號。
（2）若圖中所有的點均已確定，則找到一組解，結束，否則，將Q1、Q2清空，並任選一個未確定的點i，將i加入隊列Q1，將i'加入隊列Q2；
（3）找到i的所有后繼。對於后繼j，若j未確定，則將j加入隊列Q1；若j'（這里的j'是指與j在同一對的另一個點）未確定，則將j'加入隊列Q2；
（4）遍歷Q2中的每個點，找到該點的所有前趨（這里需要先建一個補圖），若該前趨未確定，則將其加入隊列Q2；
（5）在（3）（4）步操作中，出現以下情況之一，則本次嘗試失敗，否則本次嘗試成功：
<1>某個已被加入隊列Q1的點被加入隊列Q2；
<2>某個已被加入隊列Q2的點被加入隊列Q1;
<3>某個j的狀態為2；
<4>某個i'或j'的狀態為1或某個i'或j'的前趨的狀態為1；
（6）若本次嘗試成功，則將Q1中的所有點的狀態改為1，將Q2中所有點的狀態改為2，轉（2），否則嘗試點i'，若仍失敗則問題無解。
該算法的時間復雜度為O(NM)（最壞情況下要嘗試所有的點，每次嘗試要遍歷所有的邊），但是在多數情況下，遠遠達不到這個上界。
具 體實現時，可以用一個數組vst來表示隊列Q1和Q2。設立兩個標志變量i1和i2（要求對於不同的i，i1和i2均不同，這樣可以避免每次嘗試都要初始 化一次，節省時間），若vst[i]=i1則表示i已被加入Q1，若vst[i]=i2則表示i已被加入Q2。不過Q1和Q2仍然是要設立的，因為遍歷 （BFS）的時候需要隊列，為了防止重復遍歷，加入Q1（或Q2）中的點的vst值必然不等於i1（或i2）。中間一旦發生矛盾，立即中止嘗試，宣告失 敗。
該算法雖然在多數情況下時間復雜度到不了O(NM)，但是綜合性能仍然不如下面的O(M)算法。不過，該算法有一個很重要的用處：求字典序最小的解！
如果原圖中的同一對點編號都是連續的（01、23、45……）則可以依次嘗試第0對、第1對……點，每對點中先嘗試編號小的，若失敗再嘗試編號大的。這樣一定能求出字典序最小的解（如果有解的話），因為一個點一旦被確定，則不可更改。
如果原圖中的同一對點編號不連續（比如03、25、14……）則按照該對點中編號小的點的編號遞增順序將每對點排序，然后依次掃描排序后的每對點，先嘗試其編號小的點，若成功則將這個點選上，否則嘗試編號大的點，若成功則選上，否則（都失敗）無解。
【O(M)算法】
根據圖的對稱性，可以將圖中所有的強連通分支全部縮成一個點（因為強連通分支中的點要么都選，要么都不選），然后按照拓撲逆序 （每次找出度為0的點，具體實現時，在建分支鄰接圖時將所有邊取反）遍歷分支鄰接圖，將這個點（表示的連通分支）選上，並將其所有對立點（注意，連通分支 的對立連通分支可能有多個，若對於兩個連通分支S1和S2，點i在S1中，點i'在S2中，則S1和S2對立）及這些對立點的前趨全部標記為不選，直到所 有點均標記為止。這一過程中必然不會出現矛盾（詳細證明過程省略，論文里有）。
無解判定：若求出所有強分支后，存在點i和i'處於同一個分支，則無解，否則必定有解。
時間復雜度：求強分支時間復雜度為O(M)，拓撲排序的時間復雜度O(M)，總時間復雜度為O(M)。
該 算法的時間復雜度低，但是只能求出任意一組解，不能保證求出解的字典序最小。當然，如果原題不需要求出具體的解，只需要判定是否有解（有的題是二分 + 2-SAT判有解的），當然應該采用這種算法，只要求強連通分支（Kosaraju、Tarjan均可，推薦后者）即可。