【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。可以發現，上面的9種限制關係中，後7種二元限制關係都可以用連邊實現，比如not(a[x] and
a[y])需要連兩條邊和，a[x] or a[y]需要連兩條邊和。而前兩種一元關係，對於a[x]（即x必選），可以通過連邊來實現，而not
a[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均可，推薦後者）即可。
模板 2 SAT 問題 2 SAT
2 sat 問題 模板 有n個布林變數 x 1 x n 另有m個需要滿足的條件，每個條件的形式都是 x i 為true false或 x j 為true false 比如 x 1 為真或 x 3 為假 x 7 為假或 x 2 為假 2 sat 問題的目標是給每個變數賦值使得所有條件得到滿足。輸入格式...
2 SAT問題的演算法
求解2 sat問題的演算法有很多，有一種效率還不錯，實現方便又理解方便的演算法。注意例子中的那個條件 x1為假或x2為真 在x1為假的時候x2可以為任意值，但在x1為真的時候,x2為滿足條件必須是真。也就是說x1為真可以推導出x2為假 x2為假可以推導出x1為真。換成一般的情況，已知xa xb 則x...
2 SAT演算法（未完）
例題 演算法 演算法所求問題 這個演算法主要是求有n個人，每個有m個要求，要求只可能是1或0的情況 及是或不是，要或不要.且每個要求只需滿足其一即可，求是否有可行的分配方案 當然，也可以求出那個可行的分配方案 演算法前置知識 tarjan求強連通分量，拓撲序 演算法主要思路 如何求出能否有一種方案使...