2-SAT
总结:
-
要有 \(2\) 个变量,形如
x1 AND x2 = true
或x1 OR x2 = true
之类的,给定 \(m\) 组限制,问在这样的限制条件下有没有一组 \(x_1,x_2,\cdots,x_n\) 满足这些限制。 -
基本思路就是对于每个 \(x_i\) 建 \(2\) 个点,分别是 \(x_i\) 的
true
和 \(x_i\) 的false
。然后连边。 -
想仔细怎么建边。这里举 \(3\) 个例子:
-
x1 AND x2 = true
。如果x1 = true
,那么x2 = true
。反之亦然。所以从 \(x_1\) 的true
向 \(x_2\) 的true
连一条有向边,从 \(x_2\) 的true
向 \(x_1\) 的true
连一条有向边, -
x1 OR x2 = true
。如果x1 = false
,那么x2 = true
;同理,如果x2 = false
,那么x1 = true
。所以从 \(x_1\) 的false
向 \(x_2\) 的true
连一条有向边,从 \(x_2\) 的false
向 \(x_1\) 的true
连一条有向边。 -
x1 = true
。考虑从 \(x_1\) 的false
向 \(x_1\) 的true
连一条有向边。如果 \(x_1\) 为false
,那么 \(x_1\) 为true
。这种逻辑显然是矛盾的。至于为什么,马上就说。
-
-
我们把边建好之后跑一遍
Tarjan
,如果 \(x_i\) 的true
和false
在同一个连通块里,就说明从 \(x_i\) 为false
可以推导出 \(x_i\) 为true
。这种逻辑显然是矛盾的,所以没有解;反之则有解。 -
可以用 \(x\) 表示
true
,用 \(x+n\) 表示false
。
代码(以 P4782 为例):
#include <bits/stdc++.h>
using namespace std;
const int MAXN = 4e6 + 5;
int n, m;
vector<int> z[MAXN];//z[x]为真,z[x + n]为假
int dfn[MAXN], low[MAXN];
int st[MAXN], tail;
bool inst[MAXN];
int belong[MAXN], cnt;
int t;
void add_edge(int i, int a, int j, int b) {
if(a == 0 && b == 0) {
z[i].push_back(j + n);
z[j].push_back(i + n);
}
else if(a == 0 && b == 1) {
z[i].push_back(j);
z[j + n].push_back(i + n);
}
else if(a == 1 && b == 0) {
z[i + n].push_back(j + n);
z[j].push_back(i);
}
else {
z[i + n].push_back(j);
z[j + n].push_back(i);
}
}
void dfs(int now) {
t++;
dfn[now] = low[now] = t;
inst[now] = true;
st[++tail] = now;
for (int i = 0; i < int(z[now].size()); i++) {
int j = z[now][i];
if (!dfn[j]) {
dfs(j);
low[now] = min(low[now], low[j]);
}
else {
if(inst[j]) low[now] = min(low[now], dfn[j]);
}
}
if(low[now] == dfn[now]) {
cnt++;
belong[now] = cnt;
while(st[tail] != now) {
belong[st[tail]] = cnt;
inst[st[tail]] = false;
tail--;
}
inst[st[tail]] = false;
tail--;
}
}
int main() {
scanf("%d%d", &n, &m);
for (int k = 1; k <= m; k++) {
int i, a, j, b;
scanf("%d%d%d%d", &i, &a, &j, &b);
add_edge(i, a, j, b);
}
for (int i = 1; i <= n + n; i++) {
if(!dfn[i]) dfs(i);
}
for (int i = 1; i <= n; i++) {
if(belong[i] == belong[i + n]) {
printf("IMPOSSIBLE");
return 0;
}
}
printf("POSSIBLE\n");
for (int i = 1; i <= n; i++) {
printf("%d ", (belong[i] < belong[i + n]));
}
return 0;
}
标签:false,int,back,tail,now,true,SAT
From: https://www.cnblogs.com/ljlbj-fengyuwuzu/p/18003011/2-SAT