SAT
给定 $n$ 个布尔变量 $x_1,x_2,\cdots,x_n$，和 $m$ 组关系，每组关系给定 $i_1,i_2,\cdots,i_k,a_1,a_2,\cdots,a_k$，表明：
\[[x_{i_1}=a_1]\lor[x_{i_2}=a_2]\lor[x_{i_3}=a_3]\lor\cdots\lor[x_{i_k}]=1\]求任意一组解。
SAT 是 Satisfiability（适应性问题）的缩写。
$k$ -SAT 是 NP 完全的，只能打暴力。但是 2-SAT 还是有比较好的做法的，可以 $\mathcal O(n)$ 给出一组可行解。
2-SAT
有 $n$ 个布尔变量 $x_1\sim x_n$，另有 $m$ 个需要满足的条件，每个条件的形式都是 $[x_i=a]\lor[x_j=b]=1$。
- 若无解，输出
IMPOSSIBLE。- 否则输出
POSSIBLE，第二行输出 $n$ 个数 $x_1,x_2,\cdots,x_n$ 表示一组可行解。
建图
「$x_i=a$ 或 $x_j=b$」明显不好做，因此可以考虑将其转化为一个「确定性」条件。
例如「$x_i=1$ 或 $x_j=0$」，那么当 $x_i=0$ 的时候，必然有 $x_j=0$。也就是说，当「$x_i=a$ 或 $x_j=b$」其中一个条件不成立时，另一个一定成立。
用一张有向图来存储这些信息，记 $i$ 表示 $x_i=1$ 的状态，$\lnot i=i+n$ 表示 $x_i=0$ 的状态。
-
$a=0,b=0$：
- $x_i=1\Rightarrow x_j=0$，建边 $i\rightarrow\lnot j$。
- $x_j=1\Rightarrow x_i=0$，建边 $j\rightarrow\lnot i$。
-
$a=0,b=1$：
- $x_i=1\Rightarrow x_j=1$，建边 $i\rightarrow j$。
- $x_j=0\Rightarrow x_i=0$，建边 $\lnot j\rightarrow\lnot i$。
-
$a=1,b=0$：
- $x_i=0\Rightarrow x_j=0$，建边 $\lnot i\rightarrow\lnot j$。
- $x_j=1\Rightarrow x_i=1$，建边 $j\rightarrow i$。
-
$a=1,b=1$：
- $x_i=0\Rightarrow x_j=1$，建边 $\lnot i\rightarrow j$。
- $x_j=0\Rightarrow x_i=1$，建边 $\lnot j\rightarrow i$。
强连通分量
假设点 $i$ 代表的成立，那么 $i$ 能够通过若干条有向边到达的所有点 $j$ 代表的状态也成立。此时，若 $i$ 能够到达 $\lnot i$，则自相矛盾，无解。
为了快速判断 $i$ 能否到达 $\lnot i$，可以通过 Tarjan 求强连通分量（SCC）。
解的构造
现在我们已经确定了有解。
显然，$i,\lnot i$ 只能有一个点被选择，考虑选则拓扑序尽可能大的点，因为这样会让这个节点「更晚被遍历」，产生冲突的概率更小。
又因为已经确定有解，因此这样一定能构造一组可行解。（可能存在其他解。）
实际实现上，可以不需要再进行一遍拓扑排序，因为 Tarjan 求出的 SCC 编号就是反拓扑序。同时，整个图有可能不连通。
AC 代码
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
//#include<bits/stdc++.h>
#include<algorithm>
#include<iostream>
#include<cstring>
#include<iomanip>
#include<cstdio>
#include<string>
#include<vector>
#include<cmath>
#include<ctime>
#include<deque>
#include<queue>
#include<stack>
#include<list>
using namespace std;
constexpr const int N=1e6;
int n;
vector<int>g[N<<2|1];
int dfn[N<<1|1],id[N<<1|1];
bool ans[N+1];
void Tarjan(int x){
static int cnt,low[N<<1|1];
static bool in[N<<1|1];
static vector<int>s;
dfn[x]=low[x]=++cnt;
in[x]=true;
s.push_back(x);
for(int i:g[x]){
if(!dfn[i]){
Tarjan(i);
low[x]=min(low[x],low[i]);
}else if(in[i]){
low[x]=min(low[x],dfn[i]);
}
}
if(dfn[x]==low[x]){
static int size=0;
size++;
while(s.back()!=x){
in[s.back()]=false;
id[s.back()]=size;
s.pop_back();
}
in[s.back()]=false;
id[s.back()]=size;
s.pop_back();
}
}
int main(){
/*freopen("test.in","r",stdin);
freopen("test.out","w",stdout);*/
ios::sync_with_stdio(false);
cin.tie(0);cout.tie(0);
int m;
cin>>n>>m;
while(m--){
int i,a,j,b;
cin>>i>>a>>j>>b;
if(!a&&!b){
g[i].push_back(j+n);
g[j].push_back(i+n);
}else if(!a&&b){
g[i].push_back(j);
g[j+n].push_back(i+n);
}else if(a&&!b){
g[j].push_back(i);
g[i+n].push_back(j+n);
}else{
g[i+n].push_back(j);
g[j+n].push_back(i);
}
}
for(int i=1;i<=(n<<1);i++){
if(!dfn[i]){
Tarjan(i);
}
}
for(int i=1;i<=n;i++){
if(id[i]==id[i+n]){
cout<<"IMPOSSIBLE\n";
return 0;
}
}
for(int i=1;i<=n;i++){
if(id[i]<id[i+n]){
ans[i]=true;
}
}
cout<<"POSSIBLE\n";
for(int i=1;i<=n;i++){
cout<<ans[i]<<' ';
}
cout.flush();
/*fclose(stdin);
fclose(stdout);*/
return 0;
}
