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

Anguei · 2018-08-22 19:51:06 · 题解

什么是 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

于是我们得到了这么一张图：

可以看到，\neg a 与 b 在同一强连通分量内，a 与 \neg b 在同一强连通分量内。同一强连通分量内的变量值一定是相等的。也就是说，如果 x 与 \neg x 在同一强连通分量内部，一定无解。反之，就一定有解了。

但是，对于一组布尔方程，可能会有多组解同时成立。要怎样判断给每个布尔变量赋的值是否恰好构成一组解呢？

这个很简单，只需要 当 x 所在的强连通分量的拓扑序在 \neg x 所在的强连通分量的拓扑序之后取 x 为真 就可以了。在使用 Tarjan 算法缩点找强连通分量的过程中，已经为每组强连通分量标记好顺序了——不过是反着的拓扑序。所以一定要写成 color[x] < color[-x] 。

时间复杂度：O(N + M)

说了这么多，咋不上代码啊？

核心代码在下面。

建图

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：

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));
}

找环

// 注意所有东西都要开两倍空间，因为每个变量存了两次
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);

输出

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("");