其他分享
首页 > 其他分享> > 2-SAT

2-SAT

作者:互联网

\(2-SAT\)

来自 \(\text{OI-WIKI}\) 和 \(\text{Anguei}\) 的题解

定义:

将两个部分拆开,分为 \(2\) 和 \(SAT\) ,有一串 \(bool\) 类型的变量,对每个元素赋值,要求满足要求。

定义 \(\neg\) 表示不行,\(\vee\) 表示 ,\(\wedge\) 表示 ,这是布尔方程的定义。

例子:

比如说邀请人来吃喜酒,夫妻二人必须去一个,但是 \(A\) 男和 \(B\) 女有矛盾,\(C\) 女和 \(D\) 男矛盾,我们需要确定是否有一个方案,能避免来的人有矛盾。

使用 布尔方程 表示上述问题:设 \(a\) 表示 \(A\) 男参加,\(B\) 女不能参加 \(\neg a\)。 \(b\) 表示 \(C\) 女参加,那么 \(\neg b\) 表示 \(D\) 男不参加。

即: \((a\vee b)\) ,变量 \(a,b\) 至少满足一个。

对于这个变量关系建立有向图,则有:\((\neg a\rightarrow b)\wedge (\neg b\rightarrow a)\) ( \(a\) 不成立则 \(b\) 一定成立)。

建图之后,就可以使用 缩点 算法来求解这类问题。

求解问题:

利用 强连通分量,对于每个变量 \(x\) ,建立两个点: \(x,\neg x\) 分别表示变量 \(x\) 取 true 和取 false

所以,图的节点个数是两倍的变量个数。在存储方式上,可以给第 \(i\) 个变量标号为 \(i\) ,其对应的反值标号为 \(i+n\)。

利用上面的变量关系,按照箭头的方向建立有向边。

  1. \(\neg a\vee b\),建立: \(a \rightarrow b \wedge \neg b \rightarrow \neg a\)

  2. \(a \vee b\) ,建立:\(\neg b\rightarrow b\wedge \neg b\rightarrow a\)

  3. \(\neg a\vee \neg b\) ,建立: \(a\rightarrow \neg b\wedge b\rightarrow \neg a\)

就是从一个可以不行的状态到必须状态建一条边

然后就有这样一张图:

可以看到,同一个强连通分量内的变量值一定是相等的。也就说,如果 \(x\) 和 \(\neg x\) 在同一个强连通分量内部,一定无解,反之就一定有解了。

那么怎么判断多组布尔方程同时成立呢?

需要:当 \(x\) 所在的强连通分量的拓扑序在 \(\neg x\) 所在的强连通分量的拓扑序后取 \(x\) 为真 就行了。

在找强连通分量的过程中,已经标记了反的拓扑序,记为 \(col[x]<col[n+x]\),此时成立就标记为真,即可是最优解。

例题:

P4782 2-SAT 问题

题意:

给定 \(n\) 个布尔变量,需要有 \(m\) 个类似于: \(x_i\) 为真或 \(x_j\) 为假 的限制条件。需要给定 \(n\) 个布尔变量的赋值。

分析:

直接根据上面的建边方式跑 \(tarjan\) 就好了。

注意和其他不同的是:建立反向边,\(dfs\) 序为正。也可以建立正向边,\(dfs\) 序为反。

#include<bits/stdc++.h>

using namespace std;
const int N=3e6+5;

int n,m;

int x[N];
int dfn[N],idx,sd[N],low[N],sta[N],top,cnt,vis[N];
vector<int> g[N];

void tarjan(int x){
    dfn[x]=low[x]=++cnt;
    sta[++top]=x; vis[x]=1;
    for(auto y:g[x]){
        if(!dfn[y]){tarjan(y); low[x]=min(low[x],low[y]);}
        else if(vis[y]) low[x]=min(low[x],dfn[y]); 
    }
    if(low[x]==dfn[x]){
        idx++; int y;while(y=sta[top--]){
            sd[y]=idx; vis[y]=0;
            if(x==y) break;
        }
    }
}
int main(){
    cin>>n>>m;
    for(int i=1,x,op1,y,op2;i<=m;i++){
        scanf("%d%d%d%d",&x,&op1,&y,&op2);
        if(op1&&op2){//都存在
            g[x+n].push_back(y); g[y+n].push_back(x); 
        }
        else if(!op1&&op2){//从正x到正y,从负y到负x
            g[x].push_back(y); g[y+n].push_back(x+n);
        }
        else if(op1&&!op2){
            g[x+n].push_back(y+n); g[y].push_back(x);
        }
        else{//都不存在
            g[x].push_back(y+n); g[y].push_back(x+n);
        }
    }
    for(int i=1;i<=n*2;i++) if(!dfn[i]) tarjan(i);
    for(int i=1;i<=n;i++){
        if(sd[i]==sd[i+n]){puts("IMPOSSIBLE"); exit(0);}
    }
    puts("POSSIBLE");
    for(int i=1;i<=n;i++) printf("%d ",sd[i]<sd[i+n]?1:0); puts("");
    //强联通分量编号越大 -> 拓扑序越大(反向边) -> 越优
    system("pause");
    return 0;
}

标签:变量,int,neg,vee,low,SAT,rightarrow
来源: https://www.cnblogs.com/guanlexiangfan/p/15511023.html