首页 > 其他分享> 文章详细

2-SAT

2021-11-04 23:02:40 阅读：210 来源： 互联网

标签：变量 int neg vee low SAT rightarrow

\(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\)。

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

\(\neg a\vee b\)，建立： \(a \rightarrow b \wedge \neg b \rightarrow \neg a\)
\(a \vee b\) ，建立：\(\neg b\rightarrow b\wedge \neg b\rightarrow a\)
\(\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

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

2-SAT

\(2-SAT\)

定义：

例子：

求解问题：

例题：

P4782 2-SAT 问题

题意：

分析：