【模板】2-SAT 问题(2-SAT)

【模板】2-SAT 问题

题目背景

2-SAT 问题 模板

题目描述

有n个布尔变量 (x_1)​ ~ (x_n)​ ，另有m个需要满足的条件，每个条件的形式都是“ (x_i) 为true/false或 (x_j)​ 为true/false”。比如“ (x_1)​ 为真或 (x_3)​ 为假”、“ (x_7)​ 为假或 (x_2)​ 为假”。2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。

输入输出格式

输入格式：

第一行两个整数n和m，意义如体面所述。

接下来m行每行4个整数 i a j b，表示“ (x_i) 为a或 (x_j) 为b”(a,b∈{0,1})

输出格式：

如无解，输出“IMPOSSIBLE”（不带引号）; 否则输出"POSSIBLE"（不带引号),下 一行n个整数 (x_1) ~ (x_n)​ ((x_i)​∈{0,1})，表示构造出的解。

输入输出样例

输入样例#1： 复制

3 1
1 1 3 0

输出样例#1： 复制

POSSIBLE
0 0 0

---

题解

谈谈理解？
只会(n+m)时间复杂度的算法。
对于一个2-sat问题。有如下三种情况

1.如果A=1 那么 B=1
转化为图论思想，如果我要选A则必须选B
不选A则一定不选B
对(A,B),(B^1,A1)建边。

2.要么A=1,要么B=1
那就是
选A就不选B(A,B^1),
选B就不选A(B,A^1)

3.A一定要选
直接连边(A^1,A)
首先可以知道， (x_{i,0})​ 和 (x_{i,1})​ 必须选择且仅选择一个。那么，因为 (x_i=a) 一定满足，则 (x_i!=a) 的点不可以取。那么，直接建边 ((x_{i,aoplus1}x_{i,a})) 可以控制 (x_{i,aoplus1}), 这个点一定不可选择，否则无解。

然后用tarjan求一遍强联通分量。可以发现每一个强联通分量里面的情况是要么选就一起选，不选就一起不选的。当一个条件与它的反条件同时被选取，即在一个强联通分量时，是不成立的。要么就是成立的。

那么输出呢？怎么保证输出的方案是正确？
根据2-sat的对称原则。如果连的是双向边，那么整个图就是对称的。那么为什么比较拓扑序就一定正确呢？
因为由对称原则强联通分量一定也是相同的。而根据强联通分量被标记的时间顺序，拓扑序一定能保证每个问题有正确解。
（好吧，还是有点绕）

---

代码

#include<cstdio>
#include<cstring>
#include<iostream>
#include<algorithm>
#include<queue>
using namespace std;
const int N=3000001;
int head[N],dfn[N],low[N];
int id,tot,num,cnt;
int n,m,top;
int vis[N],line[N],bl[N];
struct node{
    int to,nex;
}e[N<<1];

int read(){
    int x=0,w=1;char ch=getchar();
    while(ch>'9'||ch<'0'){if(ch=='-')w=-1;ch=getchar();}
    while(ch>='0'&&ch<='9')x=x*10+ch-'0',ch=getchar();
    return x*w;
}

void add(int from,int to){
    num++;
    e[num].to=to;
    e[num].nex=head[from];
    head[from]=num;
}

void tarjan(int x){
    dfn[x]=low[x]=++id;
    line[++top]=x;vis[x]=1;
    for(int i=head[x];i;i=e[i].nex){
        int v=e[i].to;
        if(!dfn[v]){
            tarjan(v);
            low[x]=min(low[x],low[v]);
        }
        else if(vis[v])
        low[x]=min(low[x],dfn[v]);
    }
    if(low[x]==dfn[x]){
        cnt++;
        while(line[top+1]!=x){
            int u=line[top];
            bl[u]=cnt;
            vis[u]=0;
            top--;
        }
    }
}

bool T_sat(){
    for(int i=1;i<=n+n;i++)
    if(!dfn[i])tarjan(i);
    for(int i=1;i<=n;i++)
    if(bl[i]==bl[n+i])return false;
    return true;
}

int main(){
    n=read();m=read();
    for(int i=1;i<=m;i++){
        int x=read(),a=read(),y=read(),b=read();
        add(x+n*(a^1),y+n*b);add(y+n*(b^1),x+n*a);
    }
    if(T_sat()){
        printf("POSSIBLE
");
        for(int i=1;i<=n;i++)
        printf("%d ",bl[i]>bl[i+n]);
    }
    else printf("IMPOSSIBLE
");
    return 0;
}