「学习笔记」2-SAT

一.什么是 \(\text{2-SAT}\)

\(SAT\) 是适定性 \(Satisfiability\) 问题的简称。一般形式为 \(k -\)适定性问题,简称 \(\text{k-SAT}\)。而当 \(k>2\) 时,该问题为 \(NP\) 完全的。所以我们只研究 \(k=2\) 的情况。

形象地来说,给定 \(n\) 个布尔变量 \(a_i\),同时给出若干个约束条件:

\((\text{not})a_i\) \(op\) \((\text{not})a_j = \text{true/false}\)。

而求解 \(\text{2-SAT}\) 就是求出一组 \(a_i\) 的解。

二.将 \(\text{2-SAT}\) 问题转换为图论问题

首先定义一条有向边的定义 \(x\to y\):如果满足 \(x\) 就必须满足 \(y\)。

发现一个点有两个状态真或假,可以想到将点 \(u\) 拆为点 \(u_0,u_1\),分别表示假或真。

\(1.\) \(a\land b = \text{true}\) \(\to (a1, b1),(b1, a1)\)。

\(2.\) \(a\land b = \text{false}\) \(\to (a1, b0),(b1, a0)\)。

\(3.\) \(a\lor b = \text{true}\) \(\to (a0, b1),(b0, a1)\)。

\(4.\) \(a\lor b = \text{false}\) \(\to (a0, b0),(b0, a0)\)。

这样我们就将 \(\text{2-SAT}\) 问题转换为图论问题了,可以运用图论的方式解决。

三.解决 \(\text{2-SAT}\) 问题

  • \(1.\) 判断有无解

    由上文定义的状态可以得知,\(u_0\) 和 \(u_1\) 不能同时被满足。
    那么存在点 \(x_0\) 和 \(x_1\) 在同一个强连通分量中时,那么无解。
    反之则有解。

  • \(2.\) 求方案

    由我们的建边可得:对于每个点 \(u\),选择其拓扑序较大的那种状态更优。
    为什么呢?
    如下图所示:
    「学习笔记」2-SAT

    对于 \(x1\) 的两种状态,如果选择 \(\text{false}\),那么推导出 \(x2\) 为 \(\text{true}\),又推导出 \(x1\) 为 \(\text{true}\),又推导出 \(x2\) 为 \(\text{false}\),发现这种解法矛盾了。
    但如果对于 \(x1\) 选择 \(\text{true}\),那么 \(x2\) 为 \(\text{false}\),则满足要求。
    由此我们得出:对于每个点 \(u\),选择其拓扑序较大的那种状态更优。
    这里不需要再做一遍拓扑排序求拓扑序,在 \(\text{Tarjan}\) 求强连通分量中就求出了每个点的逆拓扑序,每个点的强连通分量编号也就是逆拓扑序。

四.例题讲解

上一篇:Hankson的趣味题


下一篇:Verilog——if语句的优先级问题