问题背景
2-SAT（2-Satisfiability）是布尔可满足性问题的一个特殊子类。给定一组布尔变量和若干限制条件，每个限制条件恰好涉及两个变量，形式为 (a ∨ b)。2-SAT问题要求判断是否存在一组变量赋值，使得所有限制条件同时满足。该问题在逻辑电路验证、软件包依赖解析、竞赛图构造等领域有广泛应用。
与一般的SAT问题（NP完全）不同，2-SAT可以在多项式时间内解决，核心思想是将布尔表达式转化为有向图，利用强连通分量（SCC）进行判定。
核心算法思想
布尔变量与蕴含图
对于每个布尔变量 x，我们引入两个节点：x（真）和 ¬x（假）。对于每个子句 (a ∨ b)，它等价于两个蕴含关系：
– ¬a → b（如果a为假，则b必须为真）
– ¬b → a（如果b为假，则a必须为真）
将所有蕴含关系构建为有向图后，2-SAT有解的充要条件是：不存在任何变量x，使得x和¬x处于同一个强连通分量中。
Tarjan算法求强连通分量
Tarjan算法基于DFS，通过维护每个节点的dfn（发现时间）和low（能回溯到的最小dfn）来识别SCC。当dfn[u] == low[u]时，说明找到了一个SCC的根节点，可以将栈中节点弹出构成一个SCC。
时间复杂度为 O(V + E)，其中V为节点数（2n），E为边数（2m）。
Java完整实现
import java.util.*;
/**
* 2-SAT问题求解器
* 使用Tarjan算法求强连通分量判定可满足性
*/
public class TwoSAT {
private int n; // 变量个数
private int varCount; // 总节点数 = 2 * n
private List<Integer>[] graph; // 蕴含图
private int[] dfn; // 发现时间
private int[] low; // 能回溯到的最小dfn
private boolean[] inStack; // 是否在栈中
private int[] sccId; // 每个节点所属的SCC编号
private int dfnIndex; // DFS时间戳
private int sccCount; // SCC计数
private Deque<Integer> stack; // Tarjan栈
public TwoSAT(int n) {
this.n = n;
this.varCount = 2 * n;
this.graph = new ArrayList[varCount];
for (int i = 0; i < varCount; i++) {
graph[i] = new ArrayList<>();
}
this.dfn = new int[varCount];
this.low = new int[varCount];
this.inStack = new boolean[varCount];
this.sccId = new int[varCount];
Arrays.fill(dfn, -1);
this.stack = new ArrayDeque<>();
}
/**
* 获取变量x的节点编号（真值节点）
* 变量i的真值节点 = 2*i, 假值节点 = 2*i+1
*/
private int var(int x, boolean isTrue) {
return 2 * x + (isTrue ? 0 : 1);
}
/**
* 获取节点v对应的否定节点
*/
private int not(int v) {
return v ^ 1;
}
/**
* 添加蕴含关系: a -> b
*/
private void addImplication(int a, int b) {
graph[a].add(b);
}
/**
* 添加子句 (a ∨ b)
* 等价于: ¬a -> b 且 ¬b -> a
*/
public void addOrClause(int a, boolean aVal, int b, boolean bVal) {
int nodeA = var(a, aVal);
int nodeB = var(b, bVal);
int notA = not(nodeA);
int notB = not(nodeB);
// ¬a -> b
addImplication(notA, nodeB);
// ¬b -> a
addImplication(notB, nodeA);
}
/**
* 强制变量x为指定值
* 等价于添加子句 (x ∨ x)
*/
public void force(int x, boolean val) {
int node = var(x, val);
int notNode = not(node);
// x -> x (自环，也可直接连not(x) -> x)
addImplication(notNode, node);
}
/**
* Tarjan DFS求强连通分量
*/
private void tarjan(int u) {
dfn[u] = low[u] = ++dfnIndex;
stack.push(u);
inStack[u] = true;
for (int v : graph[u]) {
if (dfn[v] == -1) {
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]) {
// 找到一个SCC
int w;
do {
w = stack.pop();
inStack[w] = false;
sccId[w] = sccCount;
} while (w != u);
sccCount++;
}
}
/**
* 求解2-SAT问题
* @return 若可满足返回赋值方案，否则返回null
*/
public boolean[] solve() {
// 对所有未访问节点执行Tarjan
for (int i = 0; i < varCount; i++) {
if (dfn[i] == -1) {
tarjan(i);
}
}
// 检查每个变量的真值和假值是否在同一个SCC中
boolean[] assignment = new boolean[n];
for (int i = 0; i < n; i++) {
int trueNode = var(i, true);
int falseNode = var(i, false);
if (sccId[trueNode] == sccId[falseNode]) {
return null; // 矛盾，不可满足
}
// SCC编号逆拓扑序即为赋值顺序
// 编号大的SCC先被求出，意味着拓扑序更靠后
assignment[i] = sccId[trueNode] > sccId[falseNode];
}
return assignment;
}
public static void main(String[] args) {
// 示例：3个变量，约束条件:
// (x0 ∨ x1) ∧ (¬x0 ∨ x2) ∧ (¬x1 ∨ ¬x2)
TwoSAT solver = new TwoSAT(3);
solver.addOrClause(0, true, 1, true); // x0 ∨ x1
solver.addOrClause(0, false, 2, true); // ¬x0 ∨ x2
solver.addOrClause(1, false, 2, false); // ¬x1 ∨ ¬x2
boolean[] result = solver.solve();
if (result != null) {
System.out.print("可满足，赋值方案: ");
for (int i = 0; i < result.length; i++) {
System.out.print("x" + i + "=" + result[i] + " ");
}
System.out.println();
} else {
System.out.println("不可满足");
}
// 测试不可满足情况: (x0) ∧ (¬x0)
TwoSAT solver2 = new TwoSAT(1);
solver2.force(0, true);
solver2.force(0, false);
boolean[] result2 = solver2.solve();
System.out.println(result2 == null ? "不可满足（预期结果）" : "可满足");
}
}
算法复杂度分析
- 建图时间：
O(m)，m为子句数量，每个子句添加2条有向边 - Tarjan求SCC：
O(n + m)，n为变量数 - 判定时间：
O(n)，检查每个变量的真值与假值是否同SCC - 总时间复杂度：
O(n + m) - 空间复杂度：
O(n + m)，用于存储图和辅助数组
应用场景扩展
2-SAT在竞赛编程中极为常见，典型场景包括：
– 竞赛图构造：给定向点对之间的胜负关系约束，构造合法竞赛图
– 软件包依赖：判断依赖关系是否存在冲突
– 网格染色：2-染色问题的约束满足判定
– 电路可满足性验证：限制每个门最多两个输入时的验证问题
掌握2-SAT的关键在于理解蕴含图的构造逻辑：每个子句 (a ∨ b) 等价于 ¬a → b 和 ¬b → a。一旦建立这种直觉，就能快速将各类约束转化为2-SAT模型求解。
