参考资料:2-SAT学习笔记
什么是2-SAT问题呢?
(¬a∨b∨¬c)∧(a∨b∨¬c)∧(¬a∨¬b∨c)
,给出一个类似于这样的式子,让你找出满足条件的一个解,这样的问题就是SAT问题,因为每一个括号内都有三个被限制的变量,所以这叫做3-SAT问题(是因为括号内的变量数有3个才叫3-SAT,不是因为abc才叫3-SAT)
所以2-SAT也很好理解,(¬a∨b)∧(a∨c)∧(¬c∨¬b)
就叫做 2-SAT 问题
可以证明 3-SAT 及以上的问题只能用暴力枚举解决(我也不知道怎么证明),所以我们只讨论2-SAT问题
理论知识
前置知识,你需要学会【图论】有向图的强连通分量
我们将 a V b
理解成:选择了a
就不能选b
,选择了b
就不能选a
,a
b
必须要选择一个
那我们就可以得到这样的关系:选择了a
就要选择¬b
, 选择了b
就要选择¬a
,反之也成立
根据这个关系建图,我们可以得到
我们可以看出,所有在一个强连通分量里的元素是等价的
因此,建好图之后,只要出现 x
和 ¬x
在一个强连通分量里,就说明它们等价,也就出现了矛盾,无解
接下来是一道洛谷的模板题
例题
P4782 【模板】2-SAT
题目链接
题目描述
有
n
n
n 个布尔变量
x
1
x_1
x1
∼
\sim
∼
x
n
x_n
xn,另有
m
m
m 个需要满足的条件,每个条件的形式都是 「
x
i
x_i
xi 为 true
/ false
或
x
j
x_j
xj 为 true
/ false
」。比如 「
x
1
x_1
x1 为真或
x
3
x_3
x3 为假」、「
x
7
x_7
x7 为假或
x
2
x_2
x2 为假」。
2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。
输入格式
第一行两个整数 n n n 和 m m m,意义如题面所述。
接下来 m m m 行每行 4 4 4 个整数 i i i, a a a, j j j, b b b,表示 「 x i x_i xi 为 a a a 或 x j x_j xj 为 b b b」( a , b ∈ { 0 , 1 } a, b\in \{0,1\} a,b∈{0,1})
输出格式
如无解,输出 IMPOSSIBLE
;否则输出 POSSIBLE
。
下一行 n n n 个整数 x 1 ∼ x n x_1\sim x_n x1∼xn( x i ∈ { 0 , 1 } x_i\in\{0,1\} xi∈{0,1}),表示构造出的解。
样例输入 #1
3 1
1 1 3 0
样例输出 #1
POSSIBLE
0 0 0
提示
1 ≤ n , m ≤ 1 0 6 1\leq n, m\leq 10^6 1≤n,m≤106 , 前 3 3 3 个点卡小错误,后面 5 5 5 个点卡效率。
由于数据随机生成,可能会含有( 10 0 10 0)之类的坑,但按照最常规写法的写的标程没有出错,各个数据点卡什么的提示在标程里。文章来源:https://www.toymoban.com/news/detail-827295.html
code文章来源地址https://www.toymoban.com/news/detail-827295.html
#include <bits/stdc++.h>
using namespace std;
signed main()
{
ios::sync_with_stdio(false);
cin.tie(0), cout.tie(0);
int n, m;
cin >> n >> m;
vector<vector<int>> g(2 * n + 1);
for (int i = 1; i <= m; i ++ )
{
int a, va, b, vb;
cin >> a >> va >> b >> vb;
g[a + !va * n].push_back(b + vb * n);
g[b + !vb * n].push_back(a + va * n);
// 下面四行和上两行等价
// if (va && vb) g[a].push_back(b + n), g[b].push_back(a + n);
// else if (va && !vb) g[a].push_back(b), g[b + n].push_back(a + n);
// else if (!va && vb) g[a + n].push_back(b + n), g[b].push_back(a);
// else if (!va && !vb) g[a + n].push_back(b), g[b + n].push_back(a);
}
vector<int> dfn(2 * n + 1), low(2 * n + 1), id(2 * n + 1);
vector<bool> in_stk(2 * n + 1);
int timestamp = 0, scc_cnt = 0;
stack<int> stk;
function<void(int)> tarjan = [&](int u)
{
dfn[u] = low[u] = ++ timestamp; // 先将dfn和low都初始化为时间戳
stk.push(u), in_stk[u] = true; // u加入栈中
for (int i = 0; i < g[u].size(); i ++ )
{
int j = g[u][i]; // 取出u的所有邻点j
if (!dfn[j]) // 如果j还没被遍历
{
tarjan(j);
low[u] = min(low[u], low[j]); // 用low[j]更新low[u]
}
else if (in_stk[j]) low[u] = min(low[u], dfn[j]); // 如果j已入栈 则用dfn[j]更新low[u]
}
if (dfn[u] == low[u]) // 如果该点是所在强连通分量的最高点
{
++ scc_cnt; // 强连通分量数量加一
int y;
do {
y = stk.top(); // 取出栈顶元素
stk.pop();
in_stk[y] = false;
id[y] = scc_cnt; // 标记每个点所在的连通分量编号
} while (y != u); // 直到取到此连通分量的最高点为止
}
};
for (int i = 1; i <= 2 * n; i ++ )
if (!dfn[i]) tarjan(i);
for (int i = 1; i <= n; i ++ )
if (id[i] == id[i + n])
{
cout << "IMPOSSIBLE\n";
return 0;
}
cout << "POSSIBLE\n";
for (int i = 1; i <= n; i ++ )
if (id[i] > id[i + n]) cout << 1 << ' ';
else cout << 0 << ' ';
cout << '\n';
}
到了这里,关于【图论】2-SAT的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!