2-SAT（2-Satisfiability）是布尔可满足性问题的特殊情形：每个子句恰好含两个文字。它可以在 O(V+E) 时间内判定是否有解，并构造一组合法赋值。
一、问题形式
给定 n 个布尔变量 x₁, x₂, ..., xₙ 和 m 个约束（子句），每个子句形如：
(a ∨ b) = true
其中 a, b 是文字（变量或其否定）。问是否存在一组赋值使所有子句为真。
常见约束转化
| 约束 | 等价子句 |
|---|---|
| a 必须为真 | (a ∨ a) |
| a 和 b 至少选一个 | (a ∨ b) |
| a 和 b 不能同时选 | (¬a ∨ ¬b) |
| a 和 b 必须同选/同不选 | (a∨¬b) ∧ (¬a∨b) |
| 选 a 则必须选 b | (¬a ∨ b) |
二、建图
对每个变量 xᵢ 建两个节点：xᵢ（真）和 ¬xᵢ（假），共 2n 个节点。
子句 (a ∨ b) 等价于两条蕴含：
- ¬a → b（如果 a 为假，则 b 必须为真）
- ¬b → a
// 节点编号：x_i = 2*i, ¬x_i = 2*i+1
int neg(int x) { return x ^ 1; }
void addClause(int a, int b) {
// (a ∨ b) → (¬a → b) 且 (¬b → a)
adj[neg(a)].add(b);
adj[neg(b)].add(a);
}