2-sat 相关问题总结

1.元素关系有以下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]

And 结果为1：建边 ~x->x, ~y->y (两个数都为1)

And 结果为0：建边 y->~x , x->~y(两个数至少有一个为0)

OR 结果为1：建边 ~x->y , ~y->x(两个数至少有一个为1)

OR 结果为0：建边 x->~x , y->~y(两个数都为0)

XOR 结果为1：建边 x->~y , ~x->y , ~y->x , y -> ~x (两个数一个为0，一个为1)

XOR 结果为0：建边 x->y , ~x->~y , y->x ~y->~x(两个数同为1或者同为0)

对于一般判定是不是有解的情况，我们可以直接采用tarjan算法求强联通，然后缩点，如果x与~x染色相同，说明无解，否则有解。有的时候，可能需要用二分+tarjan算法。例如：hdu3622，hdu3715等。

求字典序最小解

这里可以参看：http://www.cppblog.com/MatoNo1/archive/2011/07/13/150766.html

不过这个太麻烦了，我们可以直接暴力枚举DFS，效率也是很高的。

首先将所有的点都置为为染色，然后我们从第一个点开始DFS染色，我们先尝试将i染成红色(答案中的颜色)，将~i染成蓝色，然后dfs i的所有后继并染色，如果对于后继j没有染色，那么将j然后为红色，~j染成蓝色。如果后继j已经被染成蓝色，则说明不能选则i，如果j已经染成红色，则说明可以。那么这些后继就可以被选择。

如果选择i的时候失败了，那么必定要选择~i,如果也失败，则说明无解。否则按次序选取下一个未被染色的点。时间复杂度O(nm)。

杭电1814那个题目就是要输出最小字典序解。用第二种办法跑了500ms左右，而第一种算法则跑了3000ms左右.改到HOJ1917(只要求任意解)去测试，DFS版也只跑了0.65s的样子，而另一个则跑了3000+ms.并且前面一个写起来比较蛋碎。。。具体的程序见下。

求任意解

直接tarjan求强连通，缩点再加拓扑排序。O(M)

论文可以参看赵爽的2-SAT解法浅析论文与对称性解决2-sat的PPT

Peaceful Commission

/*
author    : csuchenan
prog      : hdu 1814
algorithm : 2-sat 暴力
2012-10-26 17:36:16	Accepted	1814	500MS	1044K	1550 B
*/
#include <cstdio>
#include <cstring>
#include <vector>
using std::vector;
#define R 1
#define B 2
#define W 0
const int maxn = 16005;
int col[maxn];
int cnt, ans[maxn];
vector<int> G[maxn];
int n, m;
bool read(){
if(scanf("%d%d", &n, &m)==EOF)
return false;
n = n<<1;
for(int i = 0; i < n; i ++)
G[i].clear();
while(m--){
int a, b;
scanf("%d%d", &a, &b);
a --;
b --;
G[a].push_back(b^1);
G[b].push_back(a^1);
}
return true;
}

bool dfs(int v){
int size = G[v].size();
if(col[v] == B)
return false;
if(col[v] == R)
return true;
col[v] = R;
col[v^1] = B;
ans[cnt ++] = v;
for(int i = 0; i != size ; i ++){
int u = G[v][i];
if(!dfs(u))
return false;
}
return true;
}

bool solve(){
memset(col, 0, sizeof(col));
for(int i = 0; i < n; i ++){
if(col[i])
continue;
cnt = 0;
if(!dfs(i)){
for(int j = 0; j < cnt; j ++){
col[ans[j]] = W;
col[ans[j]^1] = W;
}
if(!dfs(i^1))
return false;
}
}
return true;
}

int main(){
while(read()){
if(solve()){
for(int i = 0; i < n; i ++){
if(col[i]==R)
printf("%d\n", i+1);
}
}
else{
printf("NIE\n");
}
}
return 0;
}