【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……）則按照該對點中編號小的點的編號遞增順序將每對點排序，然后依次掃描排序后的每對點，先嘗試其編號小的點，若成功則將這個點選上，否則嘗試編號大的點，若成功則選上，否則（都失敗）無解。
【具體題目】
HDU1814（求字典序最小的解）
#include <iostream>
#include <stdio.h>
using namespace std;
#define re(i, n) for (int i=0; i<n; i++)
const int MAXN = 20000, MAXM = 100000, INF = ~0U >> 2;
struct node {
int a, b, pre, next;
} E[MAXM], E2[MAXM];
int _n, n, m, V[MAXN], ST[MAXN][2], Q[MAXN], Q2[MAXN], vst[MAXN];
bool res_ex;
void init_d()
{
re(i, n) E[i].a = E[i].pre = E[i].next = E2[i].a = E2[i].pre = E2[i].next = i;
m = n;
}
void add_edge(int a, int b)
{
E[m].a = a; E[m].b = b; E[m].pre = E[a].pre; E[m].next = a; E[a].pre = m; E[E[m].pre].next = m;
E2[m].a = b; E2[m].b = a; E2[m].pre = E2[b].pre; E2[m].next = b; E2[b].pre = m; E2[E2[m].pre].next = m++;
}
void solve()
{
re(i, n) {V[i] = 0; vst[i] = 0;} res_ex = 1;
int i, i1, i2, j, k, len, front, rear, front2, rear2;
bool ff;
re(_i, _n) {
if (V[_i << 1] == 1 || V[(_i << 1) + 1] == 1) continue;
i = _i << 1; len = 0;
if (!V[i]) {
ST[len][0] = i; ST[len++][1] = 1; if (!V[i ^ 1]) {ST[len][0] = i ^ 1; ST[len++][1] = 2;}
Q[front = rear = 0] = i; vst[i] = i1 = n + i; Q2[front2 = rear2 = 0] = i ^ 1; vst[i ^ 1] = i2 = (n << 1) + i; ff = 1;
for (; front<=rear; front++) {
j = Q[front];
for (int p = E[j].next; p != j; p=E[p].next) {
k = E[p].b;
if (V[k] == 2 || vst[k] == i2 || V[k ^ 1] == 1 || vst[k ^ 1] == i1) {ff = 0; break;}
if (vst[k] != i1) {
Q[++rear] = k; vst[k] = i1;
if (!V[k]) {ST[len][0] = k; ST[len++][1] = 1;}
}
if (vst[k ^ 1] != i2) {
Q2[++rear2] = k ^ 1; vst[k ^ 1] = i2;
if (!V[k]) {ST[len][0] = k ^ 1; ST[len++][1] = 2;}
}
}
if (!ff) break;
}
if (ff) {
for (; front2<=rear2; front2++) {
j = Q2[front2];
for (int p = E2[j].next; p != j; p=E2[p].next) {
k = E2[p].b;
if (V[k] == 1 || vst[k] == i1) {ff = 0; break;}
if (vst[k] != i2) {
vst[k] = i2; Q2[++rear] = k;
if (!V[k]) {ST[len][0] = k; ST[len++][1] = 2;}
}
}
if (!ff) break;
}
if (ff) {
re(j, len) V[ST[j][0]] = ST[j][1];
continue;
}
}
}
i = (_i << 1) + 1; len = 0;
if (!V[i]) {
ST[len][0] = i; ST[len++][1] = 1; if (!V[i ^ 1]) {ST[len][0] = i ^ 1; ST[len++][1] = 2;}
Q[front = rear = 0] = i; vst[i] = i1 = n + i; Q2[front2 = rear2 = 0] = i ^ 1; vst[i ^ 1] = i2 = (n << 1) + i; ff = 1;
for (; front<=rear; front++) {
j = Q[front];
for (int p = E[j].next; p != j; p=E[p].next) {
k = E[p].b;
if (V[k] == 2 || vst[k] == i2 || V[k ^ 1] == 1 || vst[k ^ 1] == i1) {ff = 0; break;}
if (vst[k] != i1) {
Q[++rear] = k; vst[k] = i1;
if (!V[k]) {ST[len][0] = k; ST[len++][1] = 1;}
}
if (vst[k ^ 1] != i2) {
Q2[++rear2] = k ^ 1; vst[k ^ 1] = i2;
if (!V[k]) {ST[len][0] = k ^ 1; ST[len++][1] = 2;}
}
}
if (!ff) break;
}
if (ff) {
for (; front2<=rear2; front2++) {
j = Q2[front2];
for (int p = E2[j].next; p != j; p=E2[p].next) {
k = E2[p].b;
if (V[k] == 1 || vst[k] == i1) {ff = 0; break;}
if (vst[k] != i2) {
vst[k] = i2; Q2[++rear] = k;
if (!V[k]) {ST[len][0] = k; ST[len++][1] = 2;}
}
}
if (!ff) break;
}
if (ff) {
re(j, len) V[ST[j][0]] = ST[j][1];
continue;
}
}
}
if (V[_i << 1] + V[(_i << 1) + 1] != 3) {res_ex = 0; break;}
}
}
int main()
{
int _m, a, b;
while (scanf("%d%d", &_n, &_m) != EOF) {
n = _n << 1; init_d();
re(i, _m) {
scanf("%d%d", &a, &b); a--; b--;
if (a != (b ^ 1)) {add_edge(a, b ^ 1); add_edge(b, a ^ 1);}
}
solve();
if (res_ex) {re(i, n) if (V[i] == 1) printf("%d\n", i + 1);} else puts("NIE");
}
return 0;
}
【O(M)算法】
根據圖的對稱性，可以將圖中所有的強連通分支全部縮成一個點（因為強連通分支中的點要么都選，要么都不選），然后按照拓撲逆序（每次找出度為0的點，具體實現時，在建分支鄰接圖時將所有邊取反）遍歷分支鄰接圖，將這個點（表示的連通分支）選上，并將其所有對立點（注意，連通分支的對立連通分支可能有多個，若對于兩個連通分支S1和S2，點i在S1中，點i'在S2中，則S1和S2對立）及這些對立點的前趨全部標記為不選，直到所有點均標記為止。這一過程中必然不會出現矛盾（詳細證明過程省略，論文里有）。
無解判定：若求出所有強分支后，存在點i和i'處于同一個分支，則無解，否則必定有解。
時間復雜度：求強分支時間復雜度為O(M)，拓撲排序的時間復雜度O(M)，總時間復雜度為O(M)。
該算法的時間復雜度低，但是只能求出任意一組解，不能保證求出解的字典序最小。當然，如果原題不需要求出具體的解，只需要判定是否有解（有的題是二分 + 2-SAT判有解的），當然應該采用這種算法，只要求強連通分支（Kosaraju、Tarjan均可，推薦后者）即可。
【具體題目】
PKU3648（本題的特殊情況非常多，具體見Discuss）
#include <iostream>
#include <stdio.h>
using namespace std;
#define re(i, n) for (int i=0; i<n; i++)
#define re2(i, l, r) for (int i=l; i<r; i++)
#define re3(i, l, r) for (int i=l; i<=r; i++)
const int MAXN = 1000, MAXM = 10000, INF = ~0U >> 2;
struct edge {
int a, b, pre, next;
} E[MAXM], E2[MAXM];
int n, n2, m, m2, stk[MAXN], stk0[MAXN], V[MAXN], w[MAXN], st[MAXN], dfn[MAXN], low[MAXN], sw[MAXN], L[MAXN], R[MAXN];
int V2[MAXN], Q[MAXN], de[MAXN], Q0[MAXN];
bool vst[MAXN], res[MAXN], res_ex;
void init_d()
{
re(i, n) E[i].a = E[i].pre = E[i].next = i;
m = n;
}
void init_d2()
{
re(i, n2) {E2[i].a = E2[i].pre = E2[i].next = i; de[i] = 0;}
m2 = n2;
}
void add_edge(int a, int b)
{
E[m].a = a; E[m].b = b; E[m].pre = E[a].pre; E[m].next = a; E[a].pre = m; E[E[m].pre].next = m++;
de[b]++;
}
void add_edge2(int a, int b)
{
E2[m2].a = a; E2[m2].b = b; E2[m2].pre = E2[a].pre; E2[m2].next = a; E2[a].pre = m2; E[E[m2].pre].next = m2++;
}
void solve()
{
int tp, tp0, x0, x, y, ord = 0, ord0 = 0; n2 = 0;
bool fd;
res_ex = 1; re(i, n) V[i] = 0;
re(i, n) if (!V[i]) {
stk[tp = 0] = stk0[tp0 = 0] = i; V[i] = 1; dfn[i] = low[i] = ++ord; st[i] = E[i].next;
while (tp0 >= 0) {
x = stk0[tp0]; fd = 0;
for (int p=st[x]; p != x; p = E[p].next) {
y = E[p].b;
if (!V[y]) {
stk[++tp] = stk0[++tp0] = y; V[y] = 1; dfn[y] = low[y] = ++ord; st[y] = E[y].next; st[x] = E[p].next; fd = 1; break;
} else if (V[y] == 1 && dfn[y] < low[x]) low[x] = dfn[y];
}
if (!fd) {
V[x] = 2;
if (low[x] == dfn[x]) {
L[n2] = ord0;
while ((y = stk[tp]) != x) {w[y] = n2; sw[ord0++] = y; tp--;}
w[stk[tp--]] = n2; sw[ord0] = x; R[n2++] = ord0++;
};
if (tp0) {x0 = stk0[tp0 - 1]; if (low[x] < low[x0]) low[x0] = low[x];} tp0--;
}
}
}
re(i, n) if (w[i] == w[i ^ 1]) {res_ex = 0; return;}
init_d2();
re2(i, n, m) {
x = w[E[i].a]; y = w[E[i].b];
if (x != y) add_edge2(y, x);
}
int front = 0, rear = -1, front0, rear0; re(i, n2) {if (!de[i]) Q[++rear] = i; V2[i] = 0;}
for (; front<=rear; front++) {
int i = Q[front], j, j0;
if (!V2[i]) {
V2[i] = 1; front0 = 0; rear0 = -1;
re(k, n2) vst[k] = 0;
re3(x, L[i], R[i]) {
j = w[sw[x] ^ 1]; Q0[++rear0] = j; vst[j] = 1;
}
for (; front0<=rear0; front0++) {
j = Q0[front0]; V2[j] = 2;
for (int p=E2[j].next; p != j; p=E2[p].next) {
j0 = E2[p].b;
if (!vst[j0]) {Q0[++rear0] = j0; vst[j0] = 1;}
}
}
}
for (int p=E[i].next; p != i; p=E[p].next) {
j = E[p].b; de[j]--;
if (!de[j]) Q[++rear] = j;
}
}
re(i, n) res[i] = 0;
re(i, n2) if (V2[i] == 1) re3(j, L[i], R[i]) res[sw[j]] = 1;
}
int main()
{
int n0, m0, x1, x2, N1, N2;
char c1, c2;
while (1) {
scanf("%d%d", &n0, &m0); if (!n0 && !m0) break; else {n = n0 << 1; init_d();}
re(i, m0) {
scanf("%d%c%d%c", &x1, &c1, &x2, &c2);
if (c1 == 'h') N1 = x1 << 1; else N1 = (x1 << 1) + 1;
if (c2 == 'h') N2 = x2 << 1; else N2 = (x2 << 1) + 1;
add_edge(N1 ^ 1, N2); add_edge(N2 ^ 1, N1);
}
add_edge(0, 1);
solve();
if (res_ex) {
bool spc = 0;
re(i, n) if (i != 1 && res[i]) {
if (spc) putchar(' '); else spc = 1;
printf("%d%c", i >> 1, i & 1 ? 'w' : 'h');
}
puts("");
} else puts("bad luck");
}
return 0;
}