前言
1.本文在非代码部分用 \(T\) 代替 \(true\),\(F\) 代替 \(false\)。
2.本文对于具体的问题解答,只涉及P4782 【模板】2-SAT 问题,其他类型(如连接符号为“与”、“异或”)暂不涉及。
3.请预习强连通相关知识。
4.本文中的“到达”和“可达”指由 \(i\) 点经过一些单向边后可以到达 \(j\) 点。
5.本文中的 \(\oplus\) 代表异或运算。
SAT(SATISFIABILITY)
中文名是布尔可满足性问题,又名命题可满足性问题。
本人不会。
2-SAT
目前只有 \(2-SAT\) 问题可以用非暴力方法解决。一般问题见P4782 【模板】2-SAT 问题。
一般来说, \(O(2^n)\) 的枚举做法适用于所有 \(SAT\) 问题,同样适用于 \(2-SAT\) 问题。但既然把 \(2-SAT\) 单独拿出来讲,那么这个问题一定就有更优的方法:就是在多项式时间复杂度中用图去解决。
考虑 \(2\) 这个数的性质,想像在C++语言下形似这些表达式的式子:
((! x[i]) && x[j]) == true [1]
(x[i] || (! x[j])) == true [2]
(x[i] ^ (! x[j])) == true [3]
我们会发现,当知道 \(x_i\) 和 \(x_j\) 其中一个布尔变量的值时,我们就有可能将另一个值求出来(当然第一个的值可以直接推得)。
而在 \([2]\) 式中,若已知 $x_i= F $ 或 \(x_j = T\),就可以得到另一个变量的值;但若已知 \(x_i=T\) 或 \(x_j=F\),另一个变量就可以任取。
大家自己想一想 \([3]\) 式。
所以在本题中,我们就可以利用这一个性质进行问题的判断有无解以及求一个解。
具体解答
对于上文的性质以及所对应的约束条件,我们可以进行建图。
对于每个布尔变量 \(x_i\) 建立两个点 \(a_{i,0}\) 和 \(a_{i,1}\),分别代表 \(x_i=F\) 和 \(x_i=T\) 这两种情况,而我们若连单向边 \(a_{p, 0} \to a_{q,1}\),则表示:若 \(x_p = F\) 则 \(x_q = T\) (当然,如果:1.若 \(x_p=T\),则我们不能通过这条边求出 \(x_q\) ;2.若 \(x_q=T\), 我们也无法通过这条边求出 \(x_p\))。
性质一
因为成立性的传递,所以若 \(a_{i,0}\) (即 \(x_i = F\))成立且能够通过单向边到达 \(a_{j,0}\),则 \(a_{j,0}\) (即 \(x_j=F\))必须成立,否则原表达式组不成立。
性质二
当:由 \(a_{i,0}\) 可以到达 \(a_{i,1}\) 且由 \(a_{i,1}\) 可以到达 \(a_{i,0}\) 时,原表达式组不成立。
因为很显然,\(a_{i,0}\) 的情况(即 \(x_i = F\)) 和 \(a_{i,1}\) 的情况(即 \(x_i=T\))有且只有一个会成立。
当满足上述条件时,要么两个条件都满足,否则就都不满足。这显然与我们的要求和实际不符合。
性质三
本问题的建图具有对称性,即:若存在边 \(a_{p, 0} \to a_{q,1}\),则一定存在 \(a_{q,0} \to a_{p,1}\)。扩展结论,可得:若 \(a_{p,0}\) 可达 \(a_{q,1}\),则 \(a_{q,0}\) 可达 \(a_{p,1}\)。
我们可以通过对原表达式分析得出这个结论。
性质四
在有解的情况下,若 \(a_{i,0}\) 能够到达 \(a_{i,1}\),那么 \(a_{i,1}\) 一定成立。
Tarjan 缩点解决
观察性质一和二,很容易想到缩点后进行某些操作来求解。
当然,若 \(a_{i,0}\) 和 \(a_{i,1}\) 被缩进一个点中,则原表达式组不成立。
然后,我们就得到了一个简单有向无环图。
这时感性理解一下,缩点后的图仍然满足对称性(比较显然)。
这是我们可以对新图进行拓扑排序。
就算有不同的拓扑序,总有一个很神奇的性质:
性质五(极其重要)
设:
\(a_{i,p}\) 的拓扑序为 \(f(a_{i,p})\)。
引理:
此时对于原表达式组一定有解,且对于任意拓扑序都有其中一组解满足:
若 \(f(a_{i,0})<f(a_{i,1})\) 则 \(a_{i,0}=T,x_i = F\),否则 \(a_{i, 1}=T,x_i = T\)。
证:
设存在 \(a_{i,p}, a_{i,p \oplus 1},a_{j,q},a_{j,q \oplus 1}\)。
又不妨设:
\[f(a_{i,p})<f(a_{i,p \oplus 1}), f(a_{j, q}) < f(a_{j,q \oplus 1}) \]根据原命题,所以:
\[a_{i,p}=a_{j,q}=T,a_{i,p\oplus 1}=a_{j,q\oplus 1}=F \]分类讨论:
一、
\(a_{i,p\oplus 1}\) 不可达 \(a_{j, q}\)。
由性质三可知,一定有 \(a_{j,q\oplus 1}\) 不可达 \(a_{i, p}\)。
1.\(a_{i,p\oplus 1}\) 不可达 \(a_{j,q\oplus 1}\):
所以 \(a_{j,q}\) 不可达 \(a_{i,p}\)。
所以没有约束关系,这部分正确。
2.\(a_{i,p\oplus 1}\) 可达 \(a_{j, q\oplus 1}\):
所以 \(a_{j,q}\) 可达 \(a_{i, p}\)。
我们知道 \(a_{i,p}=a_{j,q}=T,a_{i,p\oplus 1}=a_{j,q\oplus 1}=F\),所以满足条件。
二、
\(a_{i,p\oplus 1}\) 可达 \(a_{j,q}\)。
由性质三可知,一定有 \(a_{j,q\oplus 1}\) 可达 \(a_{i,p}\)。
因为 \(a_{i,p\oplus 1}\) 可达 \(a_{j,q}\),所以:
\[f(a_{j,q})>f(a_{i,p\oplus 1}) \]因为 \(a_{j,q\oplus 1}\) 可达 \(a_{i,p}\),所以:
\[f(a_{i,p})>f(a_{j,q\oplus 1}) \]因为 \(f(a_{i,p})<f(a_{i,p\oplus 1})\),所以:
\[f(a_{j,q\oplus 1})<f(a_{i,p})<f(a_{i,p\oplus 1})<f(a_{j,q}) \]这与我们规定的 \(f(a_{j,q})<f(a_{j,q\oplus1})\) 冲突,故这种情况不成立。
三、
\(i,j\)可交换,如上同理,成立。
故对于任意 \(i,j\) 都满足条件。
即证。
然后我们利用这个性质,就可以解决构造解的问题了。
Code
#include <bits/stdc++.h>
using namespace std;
int n, m, x, y, a, b;
int firs[2000005], nex[2000005], to[2000005], tot;
int idx, dfn[2000005], low[2000005], sta[2000005], top, cnt, bel[2000005];
bool vis[2000005];
void Add (int u, int v){
++ tot;
nex[tot] = firs[u];
firs[u] = tot;
to[tot] = v;
}
int G (int i, int j){
return i + j * n;
}
void Tarjan (int u){
if (dfn[u])
return ;
dfn[u] = low[u] = ++ idx;
sta[++ top] = u;
vis[u] = true;
for (int e = firs[u];e;e = nex[e]){
int v = to[e];
if (! dfn[v]){
Tarjan (v);
low[u] = min (low[u], low[v]);
} else
if (vis[v])
low[u] = min (low[u], dfn[v]);
}
if (dfn[u] == low[u]){
int v;
++ cnt;
do {
v = sta[top --];
bel[v] = cnt;
vis[v] = false;
} while (u != v);
}
}
int main (){
scanf ("%d%d", &n, &m);
for (int i = 1;i <= m;++ i){
scanf ("%d%d%d%d", &x, &a, &y, &b);
Add (G (x, a ^ 1), G (y, b));
Add (G (y, b ^ 1), G (x, a));
}
for (int i = 1;i <= (n << 1);++ i)
Tarjan (i);
for (int i = 1;i <= n;++ i)
if (bel[G (i, 0)] == bel[G (i, 1)]){
printf ("IMPOSSIBLE\n");
return 0;
}
printf ("POSSIBLE\n");
for (int i = 1;i <= n;++ i)
printf ("%d ", (int) (bel[G (i, 1)] < bel[G (i, 0)]));
return 0;
}
标签:2000005,入门,int,问题,low,oplus,性质,SAT
From: https://www.cnblogs.com/imcaigou/p/17883952.html