【算法】2-sat问题【模板】

什么是2-sat问题

 有n个布尔型变量xi，另外m个需要满足的条件。每个条件都是“xi为真/假或者xj为真/假”。这句话中的“或者”意味着两个条件中至少有一个正确。2-sat问题的目标是给每个变量赋值，使得所有的条件得到满足。

 算法的大致过程是这样的：

  构造一张有向图G，其中每个变量拆成两个结点2i和2i+1，分别表示xi为假和xi为真。最后要为每个变量选其中一个结点标记。

  对于每个“xi为假或者xj为假"这样的条件，我们连两条对称的有向边。我们上面说过，或者意味着两个中间至少有一个正确。所以如果xi为真的话，那么xj一定为假，所以我们从2*i+1向2*j连一条有向边。同样的道理，我们也从2*j+1向2*i连一条有向边。

  接下来我们逐一考虑每个没有赋值的变量，设为xi。我们先假定它为假，然后标记结点2i，并且沿着有向边标记所有能标记的结点。如果标记的过程中发现某个变量对应的两个结点都被标记，则xi假这个假定不成立，需要改为xi为真，然后重新标记。

  模板代码如下

  code from LRJ

  

/*
将每个变量拆成两个点2i和2i+1，分别表示xi为假和xi和真
对于每个条件，连两条对称的有向边。
逐一考虑没有赋值的变量，先假定它为假，然后标记结点2i，然后沿着有向边标记所有能标记的结点
如果标记的过程中 发现某个变量对应的两个结点都被标记，则xi为假这个假定不成立，需要改xi为真
然后重新标记
*/
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <iostream>
#include <vector>

using namespace std;
const int maxn=100+10;
struct TwoSAT{
    int n;
    vector<int>G[2*maxn];
    bool mark[maxn*2];
    int S[maxn*2],c;
    bool 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<n*2;i++)G[i].clear();
        memset(mark,0,sizeof(mark));
    }
    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);
    }

    bool solve(){
        for(int i=0;i<n*2;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;
    }
};
int main(){
return 0;
}