【模板】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,A^1)建边。
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,a\oplus1}x_{i,a})\) 可以控制 \(x_{i,a\oplus1}\), 这个点一定不可选择,否则无解。
然后用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\n");
for(int i=1;i<=n;i++)
printf("%d ",bl[i]>bl[i+n]);
}
else printf("IMPOSSIBLE\n");
return 0;
}