TwoSAT算法模板

该模板来自大白书

【解释】

给多个语句，每个语句为“ Xi为真(假) 或者 Xj为真(假)”

每个变量和拆成两个点 2*i为假， 2*i+1为真

“Xi为真 或 Xj为真”  等价于 “Xi为假 –>  Xj为真”。

DFS算法没有回溯过程。

【函数说明】

模板bfs函数在模板外一般用不到

void init(int n) :初始化

void add(int x,int xval,int y,int yval) :添加边，x,y为节点编号，xval=1表示真，xval=0表示假，yval同理

bool solve() :计算是否存在解。如果存在解返回true，不存在返回false

【变量说明】

vector<int>G[MAXN*2];//邻接表表示图。
bool mark[MAXN*2];//表示某个结点（不是变量）是否已经被访问
int s[MAXN*2],c;//s存储某次DFS访问过那些点。用于重新标记时消去之前访问过的点的记录（mark[]值）

struct Twosat
{
    int n;
    vector<int>G[MAXN*2];
    bool mark[MAXN*2];
    int s[MAXN*2],c;

    bool dfs(int x)
    {
        if(mark[x^1])return 0;//如果x^1被标记过，说明x是不成立（x^1成立），返回0
        if(mark[x])return 1;//如果x被标记过，说明x是成立的，返回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;//与之相连的变量都满足。
    }

    void init(int n)//初始化，n为变量个数（结点数2*n，从0开始）
    {
        this->n=n;
        for(int i=0;i<n*2;i++)G[i].clear();
        memset(mark,0,sizeof(mark));
    }

    void add(int x,int xval,int y,int yval)//添加边，xval=1表示真，xval=0表示假，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))//如果”Xi为假”这个假定不成立
                {
                    while(c>0)mark[s[--c]]=0;
                    if(!dfs(i+1))return 0;//改成”Xi为真”，重新标记。
                }
            }
        }
        return 1;
    }
}sat;