2-SAT问题总结

2-SAT问题总结

       2-SAT问题：n个布尔型的变量，给出m个约束条件，约束条件例如：A，B不能同时为真，A，B必须同时为真等。

       看了算法入门经典中的解决办法，关于这种解决办法比较容易理解，并且效率也不错。构造一张有向图G，其中n个变量拆成n*2个变量，也就是xi用xi*2和xi*2+1表示，如果前者标记为1，那么说明xi为真，如果后者标记为1，那么说明xi为假。对于约束条件就可进行构成边，例如xi为假或者xj为假，也就是xi为假xj必须为真，xj为假xi必须为真，这样就得到两条有向边，xi*2+1 -> xj*2    xj*2+1 -> xi*2,这样就得到了有向图G。

       有向图中所有的有向边肯定组成了若干连通分量，某一连通分量中的，一点如果为1那么，这个连通分量中的所有点都要是1，反之也是，如果某一点既为1，又为0，那么m个约束条件肯定是产生矛盾了，那么这个问题就无法解决。

       模拟这个过程的时候用的是dfs，从一点开始我们先假设这个点为0，然后从这个点开始遍历所有它能到达的点，都标记一下，如果标记过程中发现某点已经为1了，那么就以这个点为1再以这个点开始遍历，如果这个点为1为0都会产生矛盾，那么就是出现了上面的问题，约束条件产生矛盾，问题无法得到解决。sat补考一定会考原题吗，

/*********************************************2-SAT模板*********************************************/
const int maxn=10000+10;
struct TwoSAT
{int n;//原始图的节点数(未翻倍)vector<int> G[maxn*2];//G[i].j表示如果mark[i]=true,那么mark[j]也要=truebool mark[maxn*2];//标记int S[maxn*2],c;//S和c用来记录一次dfs遍历的所有节点编号//从x执行dfs遍历,途径的所有点都标记//如果不能标记,那么返回falsebool dfs(int x){if(mark[x^1]) return false;//这两句的位置不能调换if(mark[x]) return true;mark[x]=true;S[c++]=x;for(int i=0;i<G[x].size();i++)if(!dfs(G[x][i])) return false;return true;}void init(int n){this->n=n;for(int i=0;i<2*n;i++) G[i].clear();memset(mark,0,sizeof(mark));}//加入(x,xval)或(y,yval)条件//xval=0表示假，yval=1表示真void add_clause(int x,int xval,int y,int yval)//这个地方不是一尘不变的，而是参照问题的约束条件进行加边
    {x=x*2+xval;y=y*2+yval;G[x^1].push_back(y);G[y^1].push_back(x);}//判断当前2-SAT问题是否有解bool solve(){for(int i=0;i<2*n;i+=2)if(!mark[i] && !mark[i+1]){c=0;if(!dfs(i)){while(c>0) mark[S[--c]]=false;if(!dfs(i+1)) return false;}}return true;}
};
/*********************************************2-SAT模板*********************************************/