2-sat学习笔记

例：

struct TwoSAT{
    int n;
    vector<int> G[N*2];
    bool mark[N*2];
    int S[N*2],c;

    int dfs(int x)
    {
        if (mark[x^1]) return 0;
        if (mark[x]) return 1;    //和假设的值一样
        mark[x]=1;
        S[c++]=x;
        for (int i=0;i<G[x].size;i++)
            if (!dfs(G[x][i])) return 0;
        return 1; 
    }
    //x=xval or y=yval
    void add_clause(int x,int xv,int y,int yv)
    {
        x=x*2+xv;
        y=y*2+yv;
        G[x^1].push_back(y);
        G[y^1].push_back(x);
    }
  
	void init(int n)
    {
        this->n=n;
        for (int i=0;i<2*n;i++) G[i].clear();
        memset(mark,0,sizeof(mark));
    }
    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]]=0;   //清空标记 
                    if (!dfs(i+1)) return 0;
                } 
            }
        return 1;
    }
};

为什么不需要回溯呢？
因为以前定下的变量如果在一轮dfs完之后没有判为无解，那么以后新确定的变量就不会影响到它，不会因为它而无解。
由于连边的双向性（有$(x,y)$(x,y)必有$(y',x')$(y′,x′)），如果以前有个变量确定为了$x$x，dfs完之后$i$i和$i'$i′都没有被选，现在我们确定$i$i，顺着dfs确定过去是不可能找到$x'$x′的，如果那样的话，$x$x在dfs中必然可以找到$i$i。所以一轮dfs就确定了一系列点集，其它没有确定的变量就不会访问到它们了。

这个算法的最坏复杂度是$O(nm)$O(nm)的，一般达不到，好处是可以输出字典序最小的方案。

---

更常使用的是tarjan缩点求一组可行解，复杂度为$O(m)$O(m)，如果缩点后不存在$x$x和$x'$x′在同一个强联通分量内则必定有解，并可以通过拓扑排序求解（其实拓扑序就是强联通分量的编号反过来）。

关于这种算法的具体过程以及原理的证明分析可以看《由对称性解2-SAT问题》，很好地解释了为什么一定有解，以及构造解的正确性，对图的对称性有非常充分的解读。