1. 什么是 2-SAT 问题2-SAT2-Satisfiability是布尔可满足性问题SAT的一个特例其中每个子句clause恰好包含两个文字literal。给定一个由 n 个布尔变量 x₁, x₂, ..., xₙ 和 m 个子句组成的合取范式CNF公式每个子句形如 (a ∨ b)其中 a 和 b 是文字即某个变量或其否定。2-SAT 问题就是判断是否存在一组对变量的赋值真值指派使得整个公式为真可满足。与一般的 SAT 问题NP 完全问题不同2-SAT 可以在多项式时间内解决通常使用图论中的强连通分量SCC算法。2. 问题建模与图论表示解决 2-SAT 问题的核心是将逻辑公式转化为一个有向图蕴含图然后利用图的连通性进行分析。2.1 蕴含图的构建对于每个布尔变量 xᵢ我们创建两个顶点xᵢ表示 xᵢ 为真和 ¬xᵢ表示 xᵢ 为假。对于一个子句 (a ∨ b)它等价于两个逻辑蕴含如果 a 为假则 b 必须为真¬a → b如果 b 为假则 a 必须为真¬b → a我们在蕴含图中为每个蕴含关系添加一条有向边。例如对于子句 (x₁ ∨ ¬x₂)¬x₁ → ¬x₂如果 x₁ 为假则 ¬x₂ 必须为真¬(¬x₂) → x₁即 x₂ → x₁如果 ¬x₂ 为假即 x₂ 为真则 x₁ 必须为真这样我们就将 2-SAT 公式转化为了一个有 2n 个顶点、2m 条边的有向图。3. 算法原理强连通分量SCC法2-SAT 可满足的充要条件是在对应的蕴含图中对于每个变量 xᵢ顶点 xᵢ 和 ¬xᵢ 不在同一个强连通分量中。3.1 算法步骤建图根据上述规则构建蕴含图。求强连通分量使用 Kosaraju 算法或 Tarjan 算法求出图中所有强连通分量。检查矛盾对于每个变量 xᵢ检查 xᵢ 和 ¬xᵢ 是否在同一个 SCC 中。如果是则公式不可满足否则可满足。构造解如果可满足对 SCC 进行拓扑排序实际上 Tarjan 算法得到的 SCC 编号逆序就是拓扑序然后按拓扑序从后往前处理如果某个变量的真值尚未确定则将其赋值为对应 SCC 编号较小的那个文字所表示的值。4. 代码实现C以下是使用 Tarjan 算法求解 2-SAT 问题的完整实现#include iostream #include vector #include stack #include algorithm using namespace std; class TwoSAT { private: int n; // 变量个数 vectorvectorint adj; // 邻接表 vectorvectorint adjRev; // 反向图用于 Kosaraju这里用 Tarjan 不需要 // Tarjan 算法相关 vectorint dfn, low, sccId; vectorbool inStack; stackint stk; int dfsClock, sccCnt; // 变量编号转换x_i 对应 2*i¬x_i 对应 2*i1 int getIdx(int var, bool isNeg) { return 2 * var (isNeg ? 1 : 0); } void addImplication(int a, int b) { adj[a].push_back(b); } void tarjan(int u) { dfn[u] low[u] dfsClock; stk.push(u); inStack[u] true; for (int v : adj[u]) { if (!dfn[v]) { tarjan(v); low[u] min(low[u], low[v]); } else if (inStack[v]) { low[u] min(low[u], dfn[v]); } } if (dfn[u] low[u]) { int v; do { v stk.top(); stk.pop(); inStack[v] false; sccId[v] sccCnt; } while (v ! u); sccCnt; } } public: TwoSAT(int varCount) : n(varCount) { int nodeCount 2 * n; adj.resize(nodeCount); dfn.resize(nodeCount, 0); low.resize(nodeCount, 0); sccId.resize(nodeCount, -1); inStack.resize(nodeCount, false); dfsClock 0; sccCnt 0; } // 添加子句 (a ∨ b) void addClause(int aVar, bool aNeg, int bVar, bool bNeg) { int a getIdx(aVar, aNeg); int b getIdx(bVar, bNeg); // (a ∨ b) 等价于 ¬a → b 和 ¬b → a addImplication(a ^ 1, b); // ¬a → b addImplication(b ^ 1, a); // ¬b → a } // 求解 2-SAT返回是否可满足 bool solve() { // 运行 Tarjan 算法求 SCC for (int i 0; i 2 * n; i) { if (!dfn[i]) tarjan(i); } // 检查每个变量的两个文字是否在同一个 SCC for (int i 0; i n; i) { if (sccId[2 * i] sccId[2 * i 1]) { return false; // 矛盾不可满足 } } return true; } // 获取一组解假设 solve() 返回 true vectorbool getAssignment() { vectorbool assignment(n, false); for (int i 0; i n; i) { // SCC 编号小的赋值为真因为 Tarjan 得到的 SCC 编号逆序是拓扑序 assignment[i] sccId[2 * i] sccId[2 * i 1]; } return assignment; } }; int main() { // 示例3 个变量4 个子句 // 子句(x0 ∨ ¬x1), (¬x0 ∨ x2), (x1 ∨ x2), (¬x1 ∨ ¬x2) TwoSAT ts(3); ts.addClause(0, false, 1, true); // x0 ∨ ¬x1 ts.addClause(0, true, 2, false); // ¬x0 ∨ x2 ts.addClause(1, false, 2, false); // x1 ∨ x2 ts.addClause(1, true, 2, true); // ¬x1 ∨ ¬x2 if (ts.solve()) { cout Satisfiable endl; vectorbool ans ts.getAssignment(); for (int i 0; i 3; i) { cout x i (ans[i] ? true : false) endl; } } else { cout Unsatisfiable endl; } return 0; }5. 时间复杂度与空间复杂度时间复杂度O(n m)其中 n 是变量个数m 是子句个数。Tarjan 算法求 SCC 是线性的。空间复杂度O(n m)用于存储图。6. 应用场景2-SAT 问题在实际中有广泛的应用电路设计逻辑电路的可满足性检查。调度问题某些约束可表示为二元子句。图形学某些布局问题可转化为 2-SAT。编程竞赛许多题目需要将问题建模为 2-SAT 求解。7. 总结2-SAT 是 SAT 问题中可在多项式时间内解决的特例通过构建蕴含图并检查强连通分量我们可以在 O(nm) 时间内判断可满足性并构造解。掌握 2-SAT 的图论建模思想和算法实现对于解决许多约束满足问题具有重要意义。