2-SAT(心累时学习的算法)

今年noi考了一道2-SAT裸题，害怕今年省选会出到，只能填坑

SAT是适定性(Satisfiability)问题的简称 。一般形式为k-适定性问题，简称 k-SAT。
当k>2时，k-SAT是NP完全的。因此一般讨论的是k=2的情况，即2-SAT问题。
2-SAT，简单的说就是给出n个集合，每个集合有两个元素，
已知若干个

2-SAT问题

现有一个由N个布尔值组成的序列A，给出一些限制关系，比如A[x] AND A[y]=0、A[x] OR A[y] OR A[z]=1等，要确定A[0..N-1]的值，使得其满足所有限制关系。这个称为SAT问题，特别的，若每种限制关系中最多只对两个元素进行限制，则称为2-SAT问题。

由于在2-SAT问题中，最多只对两个元素进行限制，所以可能的限制关系共有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]

注意：
这里的OR是指两个条件至少有一个是正确的
比如x1和x2一共有三种组合满足“x1为真或x2为假”：
x1=1，x2=1
x1=1，x2=0
x1=0，x2=0

2-SAT的解决方法有很多，
由于博主比较蒟，所以就选择一种简单易懂的介绍一下：

算法

构造一个有向图G，每个变量xi拆成两个点2i和2i+1
分别表示xi为假，xi为真
那么对于“xi为真或xj为假”这样的条件
我们就需要连接两条边
2*i —>2*j(表示如果i为假，那么j必须是假)
2*j+1—>2*i+1(表示如果j为真，那么i必须是真)
这就有点像推导的过程
实际上每一个限制条件都会对应两条“对称”的边

接下来逐考虑每个没有赋值的变量，设为x
我们先假定x为假（为什么一定是假，约定俗成了）
之后沿着从ta出发的有向边进行标记
如果在标记过程中，发现有一个点的两种状态都被标记过了
那么我们之前的假设就被推翻了
需要改成x为真，重新标记
如果发现无论这个点赋值成真还是假，都会引起矛盾
可以证明这个2-SAT无解

可能我的叙述有点容易让读者yy
但是一定要注意：

这个算法没有回溯过程

这个课件讲的蛮好

下面给出代码：

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;
    }
};