什么是2-SAT問題呢？
我們先說一下SAT問題。給定一個布爾方程，判斷是否存在一組布爾變量的取值方案，使得整個方程式的值為真，這種問題被稱為布爾方程的可滿足性問題（SAT）。SAT問題被證明是NP完全的，當k > 2的時候我們無法在多項式時間之內求解，但是對於一些特殊的SAT（比如2-SAT）我們可以有效求解。
注：因為筆者不會打與，或，非（否定）的數學符號，所以下文中，“與”使用&&代替，“或”使用||代替，“非”使用！代替。
布爾變量只有兩個取值，0和1.
我們稱下面這種布爾方程為合取范式：
（a || b || c || ……）^ (d || e || f || g ……) ^ ……
其中a，b等等稱為文字，是一個布爾變量或其否定。使用 || 連接的部分稱為子句。如果合取范式的每個子句中的文字個數不超過兩個，那么對應的SAT問題稱為2-SAT問題。
解法：
首先，因為子句都是由不超過兩個文字組成的，用|| 表示的關系不是很好理解，我們其實要求的是滿足所有條件的一組解，也就是說其實求的是交集（&&），所以我們首先要把“a || b”的形式轉換為使用&&表示。
它的等價形式是（!a => b）&& (!b => a),其中=>是蘊含，我們可以把它理解為“推出”的意思。
它的意思是，如果a為真，那么b必然為真，否則如果a為假，那么b可以為真或者為假。
為什么呢？我們可以用現實中推理事情的過程類比一下。如果我們已知A事件，我們用A能夠推出B，那么如果A是真的，那么B必然也是真的。如果A是假的話，說明你使用了一種錯誤的方法去推B，這樣的話B的正確性就是不能確定的，所以真或者假都可以。
於是我們就可以將一個合取范式轉化為全部由“&&”連接的形式。
對於上文的轉換可以自行推一下，只要不是兩個0都是成立的。
這是對於每個子句都有兩個文字的情況，但是如果只有一個文字呢？
這里首先要說一條重要的結論：如果由！a能推出a，那么a必然為真。
我們假設一下，首先假設a為假，那么！a就是真，然后由於推出的性質，我們又能推出a為真，這與假設a為假是矛盾的。而假設a為真的話，他就是成立的。所以結論是成立的。
既然如此，對於一個單獨的文字組成的合取范式，比如（a），那就把它的否定連向它，（！a）也是一樣的。
然后對於每一個子句我們是需要建兩條邊的。因為，一個子句是兩者互相限制的，上文（a || b）的限制比較寬松，但是如果我們建立一個小型的布爾方程，我們就能看出來如果少建一條邊對於結果的影響。
比如：（b && !a && (a || !b))
對於最后一個合取范式，如果你只建一條邊的話，他就是合法的，建立兩條就是不合法的。因為如果只建一條的話，那么我們就少了一種限制，所以答案就會被影響。
不過對於一個只有一個文字的情況，我們只需要建一條邊。因為，仔細觀察的話兩邊是互相對應的。但是只有一個文字的時候，它對應的反向邊仍然是他自己，所以只用建立一條即可。
這樣的話，我們把合取范式轉化為全部由&&連接的形式，之后我們以=>建立有向邊，那么我們就有了一張有向圖。因為推出是具有傳遞性的，所以如果在這個有向圖中a能到達b，那就說明a為真的時候b一定為真。所以，在一個圖中同一個強連通分量所含的所有變量的布爾值均相同。（要么全部為真要么全部為假，否則就違反了上文）
之后我們就很容易看出，如果對於某個布爾變量x，x和！x同時存在於一個強連通分量中，那么這個布爾方程就是無解的，否則的話，我們只要先縮點，使之成為一個DAG，之后我們求出它的一個拓撲序，用上面重要的一條結論：如果由！a能推出a，那么a必然為真。來解決問題。只要在縮點之后x所在的強連通分量的拓撲序在！x所在的強連通分量的拓撲序之后，那么x即為真。
（拓撲序在前面能推出拓撲序在后面的強連通分量）
不過因為tarjan求強連通分量的時候，強連通分量的編號實際是與拓撲序相反的，所以我們不用真的縮點，直接比較一下兩個點所在的強連通分量的編號即可。
所以我們就知道了2-SAT問題的一般解法：
1.將給定的合取范式變為&&連接的表示形式。
2.以=>為關系建圖。
3.跑一遍tarjan，求出所有的布爾變量所在的強連通分量的編號。
4.首先比較每個變量所在強連通分量編號，如果自己和自己的否定在一個里面就不合法。
5.否則的話存在一組解，我們只要再比較一下每個變量自己和自己的否定的拓撲序，對其賦值即可。
我們來看一下代碼。
#include<cstdio> #include<algorithm> #include<cstring> #include<iostream> #include<cmath> #include<set> #include<queue> #define rep(i,a,n) for(int i = a;i <= n;i++) #define per(i,n,a) for(int i = n;i >= a;i--) #define enter putchar('\n') using namespace std; typedef long long ll; const int M = 1000005; const int INF = 1000000009; int read() { int ans = 0,op = 1; char ch = getchar(); while(ch < '0' || ch > '9') { if(ch == '-') op = -1; ch = getchar(); } while(ch >= '0' && ch <= '9') { ans *= 10; ans += ch - '0'; ch = getchar(); } return ans * op; } struct edge { int next,to,from; }e[M<<1]; int n,m,a,b,x,y,dfn[M<<1],low[M<<1],scc[M<<1],ecnt,idx,cnt,stack[M<<1],top,head[M<<1]; bool vis[M<<1]; void add(int x,int y) { e[++ecnt].to = y; e[ecnt].from = x; e[ecnt].next = head[x]; head[x] = ecnt; } int rev(int x) { return x > n ? x - n : x + n; } void tarjan(int x) { low[x] = dfn[x] = ++idx; vis[x] = 1,stack[++top] = x; for(int i = head[x];i;i = e[i].next) { if(!dfn[e[i].to]) tarjan(e[i].to),low[x] = min(low[x],low[e[i].to]); else if(vis[e[i].to]) low[x] = min(low[x],dfn[e[i].to]); } if(dfn[x] == low[x]) { int p; cnt++; while(p = stack[top--]) { scc[p] = cnt,vis[p] = 0; if(p == x) break; } } } int main() { n = read(),m = read(); rep(i,1,m) { a = read(),x = read(),b = read(),y = read(); if(x) a += n; if(y) b += n; add(rev(a),b),add(rev(b),a); } rep(i,1,n<<1) if(!dfn[i]) tarjan(i); rep(i,1,n) { if(scc[i] == scc[i+n]) { printf("IMPOSSIBLE\n"); return 0; } } printf("POSSIBLE\n"); rep(i,1,n) (scc[i] < scc[i+n]) ? printf("0 ") : printf("1 ");enter; return 0; }