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);
}三、判定：强连通分量
定理：2-SAT 有解 ⟺ 对任意变量 xᵢ，xᵢ 和 ¬xᵢ 不在同一个 SCC 中。
// Tarjan 求 SCC
boolean isSatisfiable() {
tarjanSCC(); // 得到 comp[] 数组
for (int i = 0; i < n; i++) {
if (comp[2 * i] == comp[2 * i + 1]) return false;
}
return true;
}四、构造解
在缩点后的 DAG 上，按拓扑逆序赋值：
boolean[] assignment = new boolean[n];
for (int i = 0; i < n; i++) {
// SCC 编号是拓扑逆序（Tarjan 的特性）
// comp 值小的在拓扑序后面
assignment[i] = comp[2 * i] > comp[2 * i + 1];
}原理：如果 xᵢ 的 SCC 在 ¬xᵢ 之后（拓扑序更大），选 xᵢ = true。
五、完整模板
public class TwoSAT {
int n;
List<Integer>[] adj;
int[] dfn, low, comp, stack;
boolean[] inStack;
int timer, top, sccCnt;
public TwoSAT(int n) {
this.n = n;
adj = new ArrayList[2 * n];
for (int i = 0; i < 2 * n; i++) adj[i] = new ArrayList<>();
dfn = new int[2 * n]; low = new int[2 * n];
comp = new int[2 * n]; stack = new int[2 * n];
inStack = new boolean[2 * n];
}
void addClause(int a, int b) {
adj[a ^ 1].add(b);
adj[b ^ 1].add(a);
}
// a 必须为真
void setTrue(int a) { addClause(a, a); }
// a 和 b 不能同时为真
void notBoth(int a, int b) { addClause(a ^ 1, b ^ 1); }
void tarjan(int u) {
dfn[u] = low[u] = ++timer;
stack[++top] = u; inStack[u] = true;
for (int v : adj[u]) {
if (dfn[v] == 0) { tarjan(v); low[u] = Math.min(low[u], low[v]); }
else if (inStack[v]) low[u] = Math.min(low[u], dfn[v]);
}
if (dfn[u] == low[u]) {
sccCnt++;
while (true) {
int w = stack[top--]; inStack[w] = false;
comp[w] = sccCnt;
if (w == u) break;
}
}
}
boolean solve(boolean[] ans) {
for (int i = 0; i < 2 * n; i++)
if (dfn[i] == 0) tarjan(i);
for (int i = 0; i < n; i++) {
if (comp[2 * i] == comp[2 * i + 1]) return false;
ans[i] = comp[2 * i] > comp[2 * i + 1];
}
return true;
}
}六、经典应用
| 问题 | 建模 |
|---|---|
| 婚礼安排（POJ 3683） | 时间段不冲突 |
| 选代表（每队选1人） | 不能同时选冲突的人 |
| 染色（相邻不同色） | 颜色约束 |
| 课程安排 | 时间冲突 |
七、面试要点
- 建图：(a∨b) → 两条蕴含边
- 判定：Tarjan SCC，x 和 ¬x 同 SCC → 无解
- 构造解：按 SCC 拓扑逆序选
- 复杂度：O(V + E) = O(n + m)
- LeetCode：无直接 2-SAT 题，但思想用于约束满足问题