标签：
2-SAT问题是这样的：有$n$个布尔变量$x_i$，另有$m$个需要满足的条件，每个条件的形式都是“$x_i$为真/假或者$x_j$为真/假”。比如："$x_1$为真或者$x_3$为假“。注意这里的”或“是指两个条件至少有一个是正确的，比如$x_1$和$x_3$一共有$3$中组合满足"$x_1$为真或者$x_3$为假“。2-SAT问题的目标是给每个变量赋值，使得所有条件得到满足。求解2-SAT问题一般比较常见方法是构造一张有向图$G$，其中每个变量$x_i$拆成两个结点$2i$和$2i+1$，分别表示$x_i$为假和$x_i$为真。最后要为每个变量选择其中一个结点标记。比如，若标记了节点$2i$，表示$x_i$为假；如果标记了$2i+1$，表示$x_i$为真。对于“$x_i$为假或者$x_j$为假”这样的条件，我们连一条有向边$2i+1 \rightarrow 2j$，表示如果标记节点$2i+1$那么也必须标记结点$j$，同理还需要连一条有向边$2j+1 \rightarrow 2i$。对于其他情况，也可以类似连边。换句话说，每个条件对应两条“对称”的边。接下来逐一考虑每个没有赋值的变量，设为$x_i$。我们首先假定它为假，然后标记借点$2_i$，并且沿着有向边标记所有能标记的结点。如果标记过程中发现某个变量对应的两个结点都被标记，则“$x_i$为假”这个假定不成立，需要改成“$x_i$为真”，然后重新标记。注意，该算法无回溯过程。如果当前考虑的变量不管赋值为真还是假都会引起矛盾，可以证明整个2-SAT问题无解（即使调整以前赋值的变量也没用）。这是很显然的，每个变量只会影响到关系到该变量的表达式的取值，因此对于未赋值的变量一定与之前的赋值无关，可以分开考虑，整个问题有解需要满足每个块都有解。下面给出求解2-SAT问题的代码：
1 struct _2_sat{ 2 int n; 3 vector<int> G[maxn << 1]; 4 bool mark[maxn << 1]; 5 int S[maxn << 1], c; 6 bool dfs(int x){ 7 if(mark[x ^ 1]) return 0; 8 if(mark[x]) return 1; 9 mark[x] = 1; 10 S[c++] = x; 11 FOR(i, 0, G[x].size() - 1) if(!dfs(G[x][i])) return 0; 12 return 1; 13 } 14 void init(int n){ 15 this->n = n; 16 FOR(i, 0, 2 * n - 1) G[i].clear(); 17 clr(mark, 0); 18 } 19 //x = xval or y = yval 20 void add_caluse(int x, int xval, int y, int yval){ 21 x = x * 2 + xval, y = y * 2 + yval; 22 G[x ^ 1].pb(y), G[y ^ 1].pb(x); 23 } 24 bool solve(){ 25 for(int i = 0; i < 2 * n; i += 2) if(!mark[i] && !mark[i + 1]){ 26 c = 0; 27 if(!dfs(i)){ 28 while(c > 0) mark[S[--c]] = 0; 29 if(!dfs(i + 1)) return 0; 30 } 31 } 32 return 1; 33 } 34 };
容易看出，这个算法的复杂度是$O(n^2)$的。
标签：
原文地址：http://www.cnblogs.com/astoninfer/p/5766961.html
