2-SAT · implication graph

2-SAT：归约成 SCC 判定

每条子句恰含两个 literal 的合取范式，判定它有没有解，是 SAT 家族里少数几个线性可解的成员。每子句三个 literal 的 3-SAT 是 NP-complete 的原型问题，而 2-SAT 落在 P 里，差别的来源相当具体：两个 literal 的析取等价于一对蕴含，于是整个公式可以画成一张有向图，可满足性变成图上的连通性问题。

本页完全建立在 SCC：Tarjan 与 Kosaraju 之上。实现层面也是如此：core/twosat.ts 里没有第二份 Tarjan，它 import 的就是 SCC 一页在用的 tarjanSteps，本页只负责把子句翻成边、再读分量编号。

1 · 从子句到蕴含边

一条子句 $(x \lor y)$ 只禁掉一种组合： $x$ 与 $y$ 同时为假。把这句话改写成蕴含，就得到两条等价的规则： $\lnot x \Rightarrow y$ ，以及 $\lnot y \Rightarrow x$ 。

定义 1.1（implication graph） 给定 $n$ 个变量、 $m$ 条子句的 2-SAT 实例，取 $2n$ 个点，每个变量 $x$ 对应两个点 $x$ 与 $\lnot x$ 。对每条子句 $(x \lor y)$ 连两条有向边 $\lnot x \to y$ 与 $\lnot y \to x$ 。所得的有向图称作该实例的 implication graph，共 $2n$ 个点、 $2m$ 条边。

同一条子句翻出的两条边互为镜像：把一条边的两端各取反再调头，就是另一条。这条性质对整张图成立， $u \to v$ 在图里， $\lnot v \to \lnot u$ 必定也在，它是后面构造解的全部依据。测试对每个实例逐边验证了这一点。

图 1-1 · 子句逐条翻成蕴含边。一帧加一条子句，两条镜像边同时亮起；可切换到不可满足的实例，看四条子句如何把两个变量的四个 literal 连成一团。

2 · 同分量即矛盾

在这张图上，一条路径就是一串推理：从 $x$ 能走到 $y$ ，意味着「若 $x$ 为真则 $y$ 必须为真」。于是判定条件可以一句话说完：实例可满足，当且仅当没有任何变量 $x$ 使得 $x$ 与 $\lnot x$ 落在同一个 strongly connected component 里。

必要性直接：同一个分量意味着 $x \Rightarrow \lnot x$ 与 $\lnot x \Rightarrow x$ 同时成立，无论给 $x$ 取哪个值都能推出它的反面。

充分性要靠上一节那条镜像性质。 $x$ 与 $\lnot x$ 分属不同分量时，把每个分量整体取真或整体取假是自洽的（分量内部互相蕴含，值必须一致），而镜像保证了「分量 $S$ 取真」与「它的镜像分量取假」这两个选择永远配对出现，不会互相打架。剩下的问题只是选哪一侧，答案在下一节。

警示 · 判定只看变量的两个 literal 是否同分量，不看它们之间有没有边。第二个预置实例里 $a$ 、 $\lnot a$ 、 $b$ 、 $\lnot b$ 四个点全在一个分量里，任取一个变量都能报出矛盾；本页的实现按变量表顺序扫，第一个撞上的是 $a$ ，但换个顺序报 $b$ 同样正确。

3 · 分量编号的比较

不可满足时给出「无解」即可，可满足时还要交出一组值。规则是： $x$ 取真，当且仅当 $x$ 所在分量在 condensation 的拓扑序上排在 $\lnot x$ 所在分量之后。直觉是把每条蕴含链尽量满足在下游：若 $x$ 在下游而 $\lnot x$ 在上游，取 $x$ 为真不会逼出任何新的矛盾。

Tarjan 白送了这个顺序。它的分量编号按出栈先后给，先出栈的一定没有出边，所以编号越小越靠拓扑序的末尾。规则因而落成一次整数比较： $\mathrm{comp}[x] < \mathrm{comp}[\lnot x]$ 时取真。整套流程是一遍 DFS 加两趟线性扫描， $O(n + m)$ 。

图 3-1 · 判定与构造的单步执行。先按出栈先后逐个定案分量，再逐变量比较两个编号；可切换到不可满足的实例，看检查在哪一个变量上停下。

注 · 比较方向依赖编号的来历，照抄会翻车。Tarjan 的编号是逆拓扑序，所以「编号小」等于「靠后」；若改用 Kosaraju，它扫出分量的顺序是正拓扑序，同一条规则必须反过来写。SCC：Tarjan 与 Kosaraju §4 把两者的产出顺序并排列了出来。本页测试把可满足实例的解写死成一组具体的值，方向写反会立刻红。

第一个预置实例的四条子句是 $(a \lor b)$ 、 $(\lnot a \lor c)$ 、 $(\lnot b \lor \lnot c)$ 、 $(a \lor c)$ ，六个 literal 缩成两个分量，恰好互为镜像： $\lbrace \lnot a, b, \lnot c \rbrace$ 与 $\lbrace a, c, \lnot b \rbrace$ ，缩点图是一条边。最初只写了前三条子句，两个分量之间一条边都没有，缩点图退化成两个孤立点，取值规则怎么写都对，方向的意义演示不出来。第四条子句 $(a \lor c)$ 是为此补上的，它把第一个分量指向第二个分量，规则这才有了可验证的方向。

4 · 参考文献

Krom, M. R. (1967). The decision problem for a class of first-order formulas in which all disjunctions are binary. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 13(1–2), 15–20.
Even, S., Itai, A., & Shamir, A. (1976). On the complexity of timetable and multicommodity flow problems. SIAM Journal on Computing, 5(4), 691–703.
Aspvall, B., Plass, M. F., & Tarjan, R. E. (1979). A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, 8(3), 121–123.