051-图论-2SAT

1. 核心概述 在布尔变量与至多二元子句的合取范式下，通过构造蕴含图并求强连通分量判定可满足性、并还原一组可行赋值，整体 O(N+E)。

2. 原文引述

Description: Calculates a valid assignment to boolean variables a, b, c,… to a 2-SAT problem, so that an expression of the type $(a||b)\&\&(!a||c)\&\&(d||!b)\&\&...$ becomes true, or reports that it is unsatisfiable. Negated variables are represented by bit-inversions (\texttt{\tilde{}x}). Time: O(N+E), where N is the number of boolean variables, and E is the number of clauses.

3. 展开阐述

• 定义与背景

  • 2-SAT：CNF 中每个子句含至多 2 个文字（变量或其否定）。可满足性可在多项式时间判定并构造证据。
  • 标准做法：将每个变量 x 拆成两个顶点 x 与 ¬x，子句 (a ∨ b) 等价于 (¬a → b) 与 (¬b → a) 的蕴含对。

• 接口/字段/数据结构（据实现习惯）

  • TwoSat(n)：初始化 n 个变量与 2n 个图节点。
  • addVar()：按需扩容变量个数。
  • either(u, v)：添加子句 (u ∨ v)，其中取反使用 ~x（即 x^1）。
  • setValue(x)：等价添加 (x ∨ x) 强制 x 为真；或添加 (¬x ∨ ¬x) 强制为假。
  • atMostOne(list)：添加“至多一个为真”的约束（常用分裂/链式辅助变量编码）。
  • solve()：返回可满足性布尔值，若为真，values[0..n-1] 给出一个 0/1 赋值。

• 核心流程/要点

  1. 蕴含图构造（2N 顶点）
     • 对每个子句 (a ∨ b) 加边 (¬a → b) 与 (¬b → a)。
     • 若需添加蕴含 a → b，可视为 (¬a ∨ b)。
  2. 强连通性判定
     • 以 Kosaraju/Tarjan 求有向图 SCC。若存在变量 x 使得 x 与 ¬x 落在同一 SCC，则不可满足（矛盾环）。
  3. 赋值还原（拓扑序）
     • 将所有 SCC 按拓扑逆序处理：若 x 与 ¬x 在不同 SCC，优先赋值“拓扑序更靠后者为真”，另一为假。实现常以 compId 比较大小决定 values[x]。
  4. 不变式与正确性直觉
     • (¬a → b) 边代表若 a 为假则 b 必真；SCC 中互相可达等价“强制相等”的一致性。
     • 拓扑逆序保证当决定 x 时，所有“必须依赖”的节点已定值，避免冲突。

• 复杂度与边界条件

  • 构图 O(E)，SCC O(N+E)，赋值 O(N)。整体 O(N+E)。
  • 边界：空子句直接不可满足；单文字子句 (a) 视作 (a ∨ a)。
  • 变量映射：常用索引 2i 表示 i 的否定/本体之一，2i^1 为补点；注意与实现保持一致。

• 变体/扩展

  • 约束编码技巧：a XOR b，a ⇒ b，恰为 k 个真/假等可用常见 2-SAT 模板编码。
  • “至多一个为真”可用链式辅助变量降到线性子句量。
  • 与最大化目标的结合：先判可行，再在可行域上二分/贪心添加限制（每轮再跑一次 2-SAT）。

• 对比与取舍

  • 与 077-图论-强连通分量：2-SAT 的判定核心即在蕴含图上做 SCC。
  • 与 SAT 一般情形：一般 CNF-SAT 为 NP 完全；2-SAT 因图结构特殊而线性可解。
  • 与简单拓扑约束：若约束能直接拓扑排序判定（无补点结构），可更轻量；2-SAT 适合带否定/或的逻辑耦合。

4. 关联节点

• 077-图论-强连通分量
• 052-图论-贝尔曼福德
• 078-图论-拓扑排序
• 015-数据结构-并查集