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

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$

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

built

可以看到,$\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("");