[图论] 2-SAT问题

2-SAT问题
有n个布尔变量xi，有m个形如”xi为真/假或者xj为真/假”的条件，求出每个xi的值，使得条件全部成立。

将变量xi拆为两个节点2i和2i+1,2i表示假，2i+1表示真。
对于一个条件”xi为真或者xj为假”，我们可以知道，若xi为真则xj必为假，那么连接2i+1->2j这条边。同样，xi为假则xj必然为真，那么连接2i->2j+1这条边。

若dfs到节点q，我们需要把所有与q相连的节点全部标记为真。如果节点q所对应的变量i已经标记。那么分为两种情况（i的情况与q相同或与q相反），与q相同则返回真，不继续dfs，与q相反则返回假，说明节点q不应该被标记。

1个变量xi只有真和假两种状态，若都不成立，那么无解。

全局变量
[cc lang=”C++”]
int n; //有多少个bool变量
vector G[MAXN * 2]; //储存图
bool mark[MAXN2]; //是否被标记
int S[MAXN2]; //失败退回
int c;
[/cc]

DFS求解过程
[cc lang=”C++”]
bool dfs(int index){
if(mark[index^1])
return false; //矛盾，标记失败
if(mark[index])
return true; //已经标记

    mark[index] = true; //标记
    S[c++] = index; //记录节点编号

    for(int i=0;i<G[index].size();i++)
        if(!dfs(G[index][i]))
            return false; //矛盾，标记失败
    return true; //index标记成功
}

[/cc]

初始化过程
[cc lang=”C++”]
void init(int n){
for(int i=0;i<2*n;i++)
G[i].clear();
memset(mark,0,sizeof(mark));
memset(S,0,sizeof(S));
}
[/cc]

获得条件，连边
[cc lang=”C++”]
void add(int x,int x_op,int y,int y_op){
x = x2 + x_op;
y = y2 + y_op;

    G[x^1].push_back(y); //第一个条件为假
    G[y^1].push_back(x); //第二个条件为假
}

[/cc]

求解
[cc lang=”C++”]
bool solve(){
for(int i=0;i<n*2;i+=2){
if(!mark[i] && !mark[i+1]){ //变量i未求解
c = 0;
if(!dfs(i)){ //i不为假
while(c>0)
mark[S[–c]] = false; //退回
if(!dfs(i+1))
return false; //i也不为真，无解
}
}
}

    return true;
}

[/cc]

BLOG