2-SAT
有 n 个布尔变量 $x_1 \sim x_n$，另有 m 个需要满足的条件，每个条件的形式都是 「$x_i$ 为 true / false 或 $x_j$ 为 true / false」。比如 「$x_1$ 为真或 $x_3$ 为假」、「$x_7$ 为假或 $x_2$ 为假」。
2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。
建立2n个点，令$x_i$表示$x_i=1$，$\neg x_i$表示$x_i=0$。
通过分析可以发现：$x_1 \or x_2 \Leftrightarrow \neg x_1 \to x_2 \Leftrightarrow \neg x_2 \to x_1$，而
| $x_1$ |
$x_2$ |
$x_1 \to x_2$ |
| 0 |
0 |
1 |
| 0 |
1 |
1 |
| 1 |
0 |
0 |
| 1 |
1 |
1 |
对于每个条件 $x_1\or x_2$，连接两条边$(\neg x_1 , x_2),(\neg x_2,x_1)$，表示若$x_1$取0，则$x_2$必然取1（$\neg x_1 \or x_2,\neg x_1 \or \neg x_2$等同理）
何时无解？
若沿着路径走出现$x_1 \to \cdots \to \neg x_1$，且$\neg x_1 \to \cdots \to x_1$时，即$x_1$可以走到$\neg x_1$，$\neg x_1$也可以走到$x_1$，也就是$x_1$和$\neg x_1$在一个强连通分量时，则一定无解（这表示无论$x_1$等于1还是0，都会出现矛盾）。
何时有解？
按上述方式连边，进行Tarjan算法，若任何一个变量$x_i$和$\neg x_i$不在同一个强连通分量中，则一定有解。
如何求解？
缩点后，求拓扑排序，枚举所有$x_i$和$\neg x_i$所在的强连通分量，取拓扑序靠后的值。
由于Tarjan算法求强连通分量的顺序是拓扑排序的逆序，因此只需取点所在强连通分量编号小的即可。正因为这样，实际求解不需要缩点。
模板题
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
| #include<bits/stdc++.h>
using namespace std;
const int N=2e6+5,M=2e6+5;
int n,m;
int h[N],to[N],ne[N],idx;
int dfn[N],low[N],timestamp;
stack<int>s;
bool ins[N];
int id[N],cnt;
void add(int a,int b){
to[idx]=b,ne[idx]=h[a],h[a]=idx++;
}
void tarjan(int u){
dfn[u]=low[u]=++timestamp;
s.push(u);
ins[u]=1;
for(int i=h[u];~i;i=ne[i]){
int j=to[i];
if(!dfn[j]){
tarjan(j);
low[u]=min(low[u],low[j]);
}
else if(ins[j]){
low[u]=min(low[u],dfn[j]);
}
}
if(low[u]==dfn[u]){
cnt++;
int k;
do{
k=s.top();
s.pop();
ins[k]=0;
id[k]=cnt;
}while(k!=u);
}
}
int main(){
ios::sync_with_stdio(false);
cin.tie(0),cout.tie(0);
cin >> n >> m;
memset(h,-1,sizeof h);
for(int k=1;k<=m;k++){
int i,a,j,b;
cin >> i >> a >> j >> b;
i--,j--;
add(2*i+!a,2*j+b);
add(2*j+!b,2*i+a);
}
for(int i=0;i<2*n;i++){
if(!dfn[i]){
tarjan(i);
}
}
for(int i=0;i<n;i++){
if(id[i*2]==id[i*2+1]){
cout << "IMPOSSIBLE\n";
return 0;
}
}
cout << "POSSIBLE\n";
for(int i=0;i<n;i++){
if(id[i*2]<id[i*2+1]){
cout << 0 << ' ';
}
else cout << 1 << ' ';
}
return 0;
}
|