2-SAT（布尔可满足性）

图算法 · 有向图连通性 · Tarjan 应用 · O(V+E)

给布尔变量找一组真值

有若干布尔变量 A, B, C… 和一堆二元子句，每个形如 (a ∨ b)（a、b 是某个变量或它的否定，至少一个为真）。问：能否给每个变量赋真/假，让所有子句同时成立？这就是 2-SAT。一般的 SAT 是 NP 完全的，但每子句只有两个文字的 2-SAT 有线性时间解法——秘密就在强连通分量。

子句变成蕴含边

把每个变量 x 拆成两个文字节点：x（取真）与 ¬x（取假），共 2n 个点。一条子句 (a ∨ b) 「至少一个为真」等价于两条蕴含：¬a → b（若 a 假，则 b 必真）和 ¬b → a。把所有子句都翻成蕴含边，得到一张蕴含图——蕴含具有传递性，正好是有向图上的可达性。

用强连通分量判定 + 赋值

在蕴含图上跑 Tarjan 求强连通分量。核心判据：若某个 x 与它的否定 ¬x 落在同一个 SCC，说明「x 真」能推出「x 假」、反之亦然——自相矛盾，无解。否则一定有解，并且赋值也现成：SCC 缩点后是 DAG，取每个变量里拓扑序更靠后的那个文字为真即可。Tarjan 给每个 SCC 的编号 comp 恰好是逆拓扑序，所以判据可写成 x = 真 ⟺ comp[x] < comp[¬x]。

下面固定 3 个变量、4 条子句 (A∨B) ∧ (A∨¬B) ∧ (A∨C) ∧ (¬A∨¬B)。点「下一步」逐步看：先逐条把子句翻成两条蕴含边，再跑 Tarjan 逐个把 SCC 着色（同色一组），然后蓝环逐变量高亮 x / ¬x 确认它们不同组（可满足），最后按 comp 逐变量赋值、节点标上真/假。走到底得到可满足解 A=真、B=假、C=真。右侧代码随每一步同步高亮。

变量 A,B,C 各拆成两个文字节点（上排正 x、下排负 ¬x），共 6 个；接下来把每条子句翻成蕴含边

1function twoSat(n: number, clauses: [number, number][]): boolean[] | null {
const g: number[][] = Array.from({ length: 2 * n }, () => []); // 2n 文字节点，蕴含图空
for (const [a, b] of clauses) {                 // 逐子句加两条蕴含边
  g[a ^ 1].push(b);                             // ¬a → b
  g[b ^ 1].push(a);                             // ¬b → a
}
const comp = tarjan(2 * n, g);                  // Tarjan 求 SCC（第 7 页），comp=逆拓扑序
for (let v = 0; v < n; v++)                     // 判定：x 与 ¬x 同组 ⟺ 无解
  if (comp[2 * v] === comp[2 * v + 1]) return null;
const assign: boolean[] = [];
for (let v = 0; v < n; v++)                     // 赋值：取拓扑序更后的文字为真
  assign.push(comp[2 * v] < comp[2 * v + 1]);
return assign;                                  // 可满足解
14}

变量3（A,B,C）

子句(A∨B) ∧ (A∨¬B) ∧ (A∨C) ∧ (¬A∨¬B)

蕴含边0 / 8

1 / 16

为什么这么快

两条蕴含：(a∨b) ⟺ ¬a→b 且 ¬b→a。
无解判据：存在变量使 x 与 ¬x 同 SCC。
赋值：否则取 comp[x] < comp[¬x]（拓扑序更后者）为真。
复杂度：建图 O(子句数) + 一趟 Tarjan O(V+E)，整体线性。

这正是强连通分量最漂亮的应用之一：SCC 不只是「找环」，它把「相互蕴含 = 必须同真同假」这件事一次性算清楚，于是一个看似组合爆炸的可满足性问题被压成了线性时间。许多约束问题（开关取舍、二选一排班、图着色的特例）都能归约成 2-SAT。

算法可视化

2-SAT（布尔可满足性）

给布尔变量找一组真值

子句变成蕴含边

用强连通分量判定 + 赋值

为什么这么快