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