2-SAT 问题 (2-Satisfiability)¶
2-SAT（2-Satisfiability）是布尔可满足性问题（SAT）在每个子句仅包含至多两个文字（Literal）时的特殊情形。与 NP-Complete 的 3-SAT 问题不同，2-SAT 问题可以在线性时间 \(\mathcal{O}(V + E)\) 内判定是否有解，并在有解时构造出一组合法赋值。
1. 问题形式化定义¶
设存在 \(n\) 个布尔变量 \(x_1, x_2, \dots, x_n \in \{0, 1\}\)，每个变量 \(x_i\) 对应原变量 \(x_i\) 与其否定 \(\neg x_i\) 两个文字。
给定 \(m\) 个由两个文字构成的析取（OR）子句：
其中 \(u_k, v_k \in \{x_i, \neg x_i\}\)。目标是为每个变量 \(x_i\) 确定一个布尔值（\(0\) 或 \(1\)），使得所有子句同时为真，或者报告无解。
2. 蕴涵图（Implication Graph）建模¶
2.1 析取向蕴涵的等价转化¶
根据数理逻辑中的蕴涵律（Implication Law）：
其直观含义为：若 \(A\) 为假，则为了满足 \(A \lor B = 1\)，\(B\) 必须为真；反之若 \(B\) 为假，则 \(A\) 必须为真。
因此，每个形如 \((u \lor v)\) 的析取子句都可以转化为两条有向约束边： - \(\neg u \to v\) - \(\neg v \to u\)
有向边 \(u \to v\) 表示：若选择了 \(u\) 为真，则必须同时选择 \(v\) 为真。
2.2 节点编号约定¶
通常为每个布尔变量 \(x_i\)（\(0 \le i < n\)）在有向图中建立两个节点： - 节点 \(2i\)：表示 \(x_i = \text{true}\) - 节点 \(2i + 1\)：表示 \(x_i = \text{false}\)（即 \(\neg x_i\)）
利用异或运算，对任意节点 \(u\)，其对立节点为 \(u \oplus 1\)。
2.3 常见约束关系的建图规则¶
| 约束描述 | 逻辑公式 | 蕴涵图有向边 |
|---|---|---|
| 至少一个为真 | \(A \lor B\) | \(\neg A \to B,\; \neg B \to A\) |
| 至多一个为真 | \(\neg A \lor \neg B\) | \(A \to \neg B,\; B \to \neg A\) |
| 必须异或（恰好一个为真） | \(A \oplus B = 1\) | \(A \to \neg B,\; \neg B \to A,\; B \to \neg A,\; \neg A \to B\) |
| 必须相同（同真或同假） | \(A \iff B\) | \(A \to B,\; B \to A,\; \neg A \to \neg B,\; \neg B \to \neg A\) |
| 变量 \(A\) 必须为真 | \(A = 1\) | \(\neg A \to A\)（若选 \(\neg A\) 则推出矛盾 \(A\)，故只能选 \(A\)） |
| 变量 \(A\) 必须为假 | \(A = 0\) | \(A \to \neg A\)（若选 \(A\) 则推出矛盾 \(\neg A\)，故只能选 \(\neg A\)） |
3. 求解算法：强连通分量（Tarjan SCC）¶
3.1 有解的充要条件¶
若在蕴涵图中存在有向路径 \(u \rightsquigarrow v\)，则根据传递性：选择 \(u\) 为真必然导致 \(v\) 为真。
定理（2-SAT 可满足性定理）：
2-SAT 问题有解的充要条件是：对于任意变量 \(x_i\)，节点 \(2i\) 与节点 \(2i+1\) 不在同一个强连通分量（SCC）中。
证明： - 必要性：若 \(2i\) 与 \(2i+1\) 在同一个强连通分量中，则蕴涵图中存在双向可达路径 \(2i \rightsquigarrow 2i+1\) 和 \(2i+1 \rightsquigarrow 2i\)。这意味着若 \(x_i = 1\) 则必须 \(x_i = 0\)，若 \(x_i = 0\) 则必须 \(x_i = 1\)，产生自相矛盾，必定无解。 - 充分性：若所有对立节点均不在同一强连通分量，将强连通分量缩点后得到有向无环图（DAG）。通过逆拓扑序可以构造出一组必定合法的真值分配。
3.2 构造合法解（拓扑排序与缩点）¶
在缩点后的 DAG 中，如果存在从 \(\operatorname{scc}(u)\) 到 \(\operatorname{scc}(v)\) 的有向路径，则我们不能同时选择 \(u\) 为真而 \(v\) 为假。
为了避免冲突，应该优先选择拓扑序靠后（出度较小/靠近汇点 Sink）的强连通分量： - 如果选择了一个靠近源点的点为真，它会顺着有向边强制激活后面的一整条链，极易引发矛盾； - 如果选择了一个靠近汇点的点为真，它不会向后激活其他点，约束最少。
根据 Tarjan 算法的运行特性：
- 节点离开递归调用栈的顺序即为强连通分量的生成顺序。
- Tarjan 算法求出的 scc_id 编号顺序恰好是 DAG 的逆拓扑序！
- 即：scc_id 较小的强连通分量在拓扑排序中更靠后（靠近汇点 Sink）。
因此，真值赋值规则为：
4. C++ 算法模板¶
#include <vector>
#include <stack>
#include <algorithm>
struct TwoSAT {
int n; // 变量个数
std::vector<std::vector<int>> adj;
std::vector<int> dfn, low, scc;
std::vector<bool> in_stack;
std::stack<int> st;
int timer, scc_count;
explicit TwoSAT(int n) : n(n), adj(2 * n), dfn(2 * n, 0), low(2 * n, 0),
scc(2 * n, -1), in_stack(2 * n, false),
timer(0), scc_count(0) {}
// 添加子句: (u == val_u) or (v == val_v)
// val_u, val_v 取值为 0 或 1
void add_clause(int u, int val_u, int v, int val_v) {
int node_u = 2 * u + (val_u ? 0 : 1);
int node_v = 2 * v + (val_v ? 0 : 1);
int not_u = node_u ^ 1;
int not_v = node_v ^ 1;
// ~u -> v
adj[not_u].push_back(node_v);
// ~v -> u
adj[not_v].push_back(node_u);
}
// 强制 u 必须为 val (val 取 0 或 1)
void add_must(int u, int val) {
int node_u = 2 * u + (val ? 0 : 1);
int not_u = node_u ^ 1;
adj[not_u].push_back(node_u);
}
void tarjan(int u) {
dfn[u] = low[u] = ++timer;
st.push(u);
in_stack[u] = true;
for (int v : adj[u]) {
if (!dfn[v]) {
tarjan(v);
low[u] = std::min(low[u], low[v]);
} else if (in_stack[v]) {
low[u] = std::min(low[u], dfn[v]);
}
}
if (low[u] == dfn[u]) {
while (true) {
int curr = st.top();
st.pop();
in_stack[curr] = false;
scc[curr] = scc_count;
if (curr == u) break;
}
scc_count++;
}
}
// 求解 2-SAT
// 返回 pair<bool, vector<int>>: 是否有解，以及每个变量的赋值 (0 或 1)
std::pair<bool, std::vector<int>> solve() {
for (int i = 0; i < 2 * n; i++) {
if (!dfn[i]) {
tarjan(i);
}
}
std::vector<int> assignment(n);
for (int i = 0; i < n; i++) {
if (scc[2 * i] == scc[2 * i + 1]) {
return {false, {}}; // 同一强连通分量，无解
}
// scc 编号较小者在逆拓扑序中更靠前 (即拓扑序更靠后，靠近汇点)
assignment[i] = (scc[2 * i] < scc[2 * i + 1]) ? 1 : 0;
}
return {true, assignment};
}
};
5. 经典例题与模型转换¶
5.1 洛谷 P4782 【模板】2-SAT 问题¶
题目大意：有 \(n\) 个布尔变量和 \(m\) 个条件，每个条件形如「\(x_i\) 为 \(a\) 或 \(x_j\) 为 \(b\)」（\(a, b \in \{0, 1\}\)）。判断是否有解，若有解输出任意一组变量取值。
题解：直接调用上述模板，将每个条件调用 add_clause(i, a, j, b)，运行 solve() 即可。时间复杂度 \(\mathcal{O}(n + m)\)。
5.2 LeetCode 经典联系：二分图染色与二元约束¶
在 LeetCode 中，纯粹的 2-SAT 原题较为罕见（通常作为 Hard 竞赛题出现），但很多二元互斥或二分决策问题与 2-SAT 思想一脉相承：
LeetCode 785. 判断二分图 / 886. 可能的二分法¶
- 问题本质：每个元素有两个对立状态（集合 \(A\) 或集合 \(B\)）。若 \(u\) 与 \(v\) 不能在同一个集合，则有约束 \(u \ne v\)。
- 联系：
- 这是一类特殊的 2-SAT：\(u = 0 \iff v = 1\)。
- 由于约束是对称的无向关系，它退化为了二分图判定（2-Coloring），可以通过简单的 BFS / DFS 染色或并查集（扩展域并查集）在线性时间求解。
2-SAT 与并查集（扩展域并查集）的关系¶
对于只包含「相等（\(A \iff B\)）」与「互斥（\(A \oplus B = 1\)）」两种对称约束的问题，不需要完整的有向强连通分量缩点，可以直接使用扩展域并查集维护： - 节点 \(i\) 表示 \(x_i = 1\)，\(i + n\) 表示 \(x_i = 0\)。 - 若 \(A\) 与 \(B\) 相同：合并 \((A, B)\) 以及 \((A + n, B + n)\)。 - 若 \(A\) 与 \(B\) 互斥：合并 \((A, B + n)\) 以及 \((A + n, B)\)。 - 若某个 \(i\) 与 \(i + n\) 被合并到了同一个连通块，说明产生逻辑冲突。 - 扩展域并查集只能处理对称约束（无向蕴涵），而一般的 2-SAT 能够处理单向蕴涵（如 \(A \to B\)，即 \(\neg A \lor B\)），必须依赖 Tarjan SCC 求解。
6. 复杂度分析与总结¶
| 特性 | 2-SAT | 3-SAT 及更高阶 SAT |
|---|---|---|
| 子句最大文字数 | 2 | \(\ge 3\) |
| 计算复杂度 | \(\mathcal{O}(V + E)\)（多项式时间 / 线性） | NP-Complete（指数级 \(\mathcal{O}(2^n)\)） |
| 核心算法 | 蕴涵图 + Tarjan SCC 缩点 + 逆拓扑序构造 | 回溯搜索 / DPLL / CDCL 求解器 |
| 适用场景 | 排班冲突判定、时间窗口匹配、芯片布线相交判定 | 复杂约束满足、逻辑推理验证、硬件形式化验证 |