题解 P4782 【【模板】2-SAT 问题】

Anguei

2018-08-22 19:51:06

Solution

## 什么是 2-SAT? 首先,把「2」和「SAT」拆开。SAT 是 Satisfiability 的缩写,意为可满足性。即一串布尔变量,每个变量只能为真或假。要求对这些变量进行赋值,满足布尔方程。 举个例子:教练正在讲授一个算法,代码要给教室中的多位同学阅读,代码的码风要满足所有学生。假设教室当中有三位学生:Anguei、Anfangen、Zachary_260325。现在他们每人有如下要求: + **Anguei**: 我要求代码当中满足下列条件之一: 1. 不写 `using namespace std;` ( $\neg a$) 2. 使用读入优化 ($b$) 3. 大括号不换行 ($\neg c$) + **Anfangen**: 我要求代码当中满足下条件之一: 1. 写 `using namespace std;` ($a$) 2. 使用读入优化 ($b$) 3. 大括号不换行 ($\neg c$) + **Zachary_260325**:我要求代码当中满足下条件之一: 1. 不写 `using namespace std;` ($\neg a$) 2. 使用 `scanf` ($\neg b$) 3. 大括号换行 ($c$) 我们不妨把三种要求设为 $a,b,c$,变量前加 $\neg$ 表示「不」,即「假」。上述条件翻译成布尔方程即:$(\neg a\vee b\vee\neg c) \wedge (a\vee b\vee\neg c) \wedge (\neg a\vee\neg b\vee c)$。其中,$\vee$ 表示或,$\wedge$ 表示与。(就像集合中并集交集一样) 现在要做的是,为 ABC 三个变量赋值,满足三位学生的要求。 Q: 这可怎么赋值啊?暴力? A: 对,这是 SAT 问题,已被证明为 **NP 完全** 的,只能暴力。 Q: 那么 2-SAT 是什么呢? A: 2-SAT,即每位同学 **只有两个条件**(比如三位同学都对大括号是否换行不做要求,这就少了一个条件)不过,仍要使所有同学得到满足。于是,以上布尔方程当中的 $c,\neg c$ 没了,变成了这个样子:$(\neg a\vee b) \wedge (a\vee b) \wedge (\neg a\vee\neg b)$ ## 怎么求解 2-SAT 问题? **使用强连通分量。** 对于每个变量 $x$,我们建立两个点:$x, \neg x$ 分别表示变量 $x$ 取 `true` 和取 `false`。所以,**图的节点个数是两倍的变量个数**。**在存储方式上,可以给第 $i$ 个变量标号为 $i$,其对应的反值标号为 $i + n$**。对于每个同学的要求 $(a \vee b)$,转换为 $\neg a\rightarrow b\wedge\neg b\rightarrow a$。对于这个式子,可以理解为:「若 $a$ 假则 $b$ 必真,若 $b$ 假则 $a$ 必真」然后按照箭头的方向建有向边就好了。综上,我们这样对上面的方程建图: | 原式 | 建图 | | :----------- | :----------- | | $\neg a\vee b$ | $a\rightarrow b\wedge\neg b\rightarrow\neg a$ | | $a \vee b$ | $\neg a\rightarrow b\wedge\neg b\rightarrow a$ | | $\neg a\vee\neg b\space \space $ | $a\rightarrow\neg b\wedge b\rightarrow\neg a$ | 于是我们得到了这么一张图: ![built](https://s1.ax1x.com/2018/08/22/PTAjy9.png) 可以看到,$\neg a$ 与 $b$ 在同一强连通分量内,$a$ 与 $\neg b$ 在同一强连通分量内。**同一强连通分量内的变量值一定是相等的**。也就是说,如果 $x$ 与 $\neg x$ 在同一强连通分量内部,一定无解。反之,就一定有解了。 但是,对于一组布尔方程,可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢? 这个很简单,只需要 **当 $x$ 所在的强连通分量的拓扑序在 $\neg x$ 所在的强连通分量的拓扑序之后取 $x$ 为真** 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中,已经为每组强连通分量标记好顺序了——**不过是反着的拓扑序**。所以一定要写成 `color[x] < color[-x]` 。 时间复杂度:$O(N + M)$ ## 说了这么多,咋不上代码啊? 核心代码在下面。 ### 建图 ```cpp n = read(), m = read(); for (int i = 0; i < m; ++i) { // 笔者习惯对 x 点标号为 x,-x 标号为 x+n,当然也可以反过来。 int a = read(), va = read(), b = read(), vb = read(); if (va && vb) { // a, b 都真,-a -> b, -b -> a g[a + n].push_back(b); g[b + n].push_back(a); } else if (!va && vb) { // a 假 b 真,a -> b, -b -> -a g[a].push_back(b); g[b + n].push_back(a + n); } else if (va && !vb) { // a 真 b 假,-a -> -b, b -> a g[a + n].push_back(b + n); g[b].push_back(a); } else if (!va && !vb) { // a, b 都假,a -> -b, b -> -a g[a].push_back(b + n); g[b].push_back(a + n); } } ``` 当然,还有更精简的位运算建图方式,可以免去上面的四个 if: ```cpp n = read(), m = read(); for (int i = 0; i < m; ++i) { int a = read(), va = read(), b = read(), vb = read(); g[a + n * (va & 1)].push_back(b + n * (vb ^ 1)); g[b + n * (vb & 1)].push_back(a + n * (va ^ 1)); } ``` ### 找环 ```cpp // 注意所有东西都要开两倍空间,因为每个变量存了两次 void tarjan(int u) { low[u] = dfn[u] = ++dfsClock; stk.push(u); ins[u] = true; for (const auto &v : g[u]) { if (!dfn[v]) tarjan(v), low[u] = std::min(low[u], low[v]); else if (ins[v]) low[u] = std::min(low[u], dfn[v]); } if (low[u] == dfn[u]) { ++sccCnt; do { color[u] = sccCnt; u = stk.top(); stk.pop(); ins[u] = false; } while (low[u] != dfn[u]); } } // 笔者使用了 Tarjan 找环,得到的 color[x] 是 x 所在的 scc 的拓扑逆序。 for (int i = 1; i <= (n << 1); ++i) if (!dfn[i]) tarjan(i); ``` ### 输出 ```cpp for (int i = 1; i <= n; ++i) if (color[i] == color[i + n]) { // x 与 -x 在同一强连通分量内,一定无解 puts("IMPOSSIBLE"); exit(0); } puts("POSSIBLE"); for (int i = 1; i <= n; ++i) print((color[i] < color[i + n])), putchar(' '); // 如果不使用 Tarjan 找环,请改成大于号 puts(""); ```