2-SAT（2-Satisfiability）是判定布尔表达式可满足性的经典问题。给定一个由若干子句构成的合取范式（CNF），每个子句恰好包含两个文字，判定是否存在一组变量赋值使整个表达式为真。本文用Java完整实现基于强连通分量（SCC）的2-SAT求解算法。
一、问题引入：会议安排冲突
假设有 n 场会议，每场会议可以在上午或下午举行。已知某些会议不能同时安排在上午，某些不能同时安排在下午，某些必须在同一时段。如何判断是否存在满足所有约束的安排方案？
将”会议i在上午”记为布尔变量 xᵢ，在下午则为 ¬xᵢ。约束”会议i和j不能同时在上午”表示为 ¬xᵢ ∨ ¬xⱼ。这就是一个典型的2-SAT问题。
二、核心定理：蕴含图与SCC
关键转化：将每个子句 a ∨ b 转化为两条蕴含关系：
¬a → b (如果a为假，则b必须为真)
¬b → a (如果b为假，则a必须为真)
蕴含图构建：
– 每个布尔变量 xᵢ 对应两个节点：i（表示 xᵢ 为真）和 i+n（表示 ¬xᵢ 为真，即 xᵢ 为假）
– 每条蕴含关系 u → v 对应一条有向边
核心定理：2-SAT问题有解，当且仅当不存在某个变量 xᵢ，使得 xᵢ 和 ¬xᵢ 在同一个强连通分量中。
求解步骤：
1. 构建蕴含图
2. 用Tarjan算法求所有强连通分量（SCC）
3. 检查每个变量的真假节点是否在同一SCC
4. 按SCC拓扑序的逆序赋值
三、完整Java实现
import java.util.*;
/**
* 2-SAT求解器
* 基于Tarjan强连通分量算法
* 时间复杂度: O(n + m)
*/
public class TwoSAT {
private int n; // 变量个数
private int size; // 节点总数 = 2*n
private List<Integer>[] graph; // 蕴含图
private List<Integer>[] revGraph; // 逆图（用于Kosaraju）
// Tarjan算法相关
private int[] dfn, low, sccId;
private boolean[] inStack;
private Deque<Integer> stack;
private int timestamp, sccCount;
/**
* 初始化2-SAT求解器
* @param n 布尔变量个数 (变量编号: 0 ~ n-1)
*/
@SuppressWarnings("unchecked")
public TwoSAT(int n) {
this.n = n;
this.size = 2 * n;
graph = new ArrayList[size];
revGraph = new ArrayList[size];
for (int i = 0; i < size; i++) {
graph[i] = new ArrayList<>();
revGraph[i] = new ArrayList<>();
}
}
/**
* 节点编码:
* i (0 <= i < n) -> x_i 为真
* i + n (0 <= i < n) -> x_i 为假 (即 ¬x_i 为真)
*/
private int varTrue(int i) { return i; }
private int varFalse(int i) { return i + n; }
/**
* 添加子句: a OR b
* 其中 a, b 为带符号的变量:
* 正数 i 表示 x_i
* 负数 -i 表示 ¬x_i (即 x_{i-1} 为假，这里采用1-based输入)
*
* 为简化API，我们提供基于0-based的子句添加方法
*/
/**
* 添加子句: (x_i = val_i) OR (x_j = val_j)
* @param i 第一个变量下标 (0-based)
* @param val_i true表示x_i, false表示¬x_i
* @param j 第二个变量下标 (0-based)
* @param val_j true表示x_j, false表示¬x_j
*/
public void addOrClause(int i, boolean val_i, int j, boolean val_j) {
int a = val_i ? varTrue(i) : varFalse(i); // 第一个文字对应的节点
int notA = val_i ? varFalse(i) : varTrue(i); // 第一个文字的否定
int b = val_j ? varTrue(j) : varFalse(j);
int notB = val_j ? varFalse(j) : varTrue(j);
// ¬a → b 和 ¬b → a
addImplication(notA, b);
addImplication(notB, a);
}
/**
* 添加约束: x_i 必须为 val
* 等价于: (x_i = val) OR (x_i = val)
*/
public void force(int i, boolean val) {
addOrClause(i, val, i, val);
}
/**
* 添加约束: x_i 和 x_j 不能同时为真
* 即: ¬x_i OR ¬x_j
*/
public void addNotBothTrue(int i, int j) {
addOrClause(i, false, j, false);
}
/**
* 添加约束: x_i 和 x_j 不能同时为假
* 即: x_i OR x_j
*/
public void addNotBothFalse(int i, int j) {
addOrClause(i, true, j, true);
}
/**
* 添加约束: x_i 和 x_j 必须相同
* 即: (x_i AND x_j) OR (¬x_i AND ¬x_j)
* 分解为: (¬x_i OR x_j) AND (x_i OR ¬x_j)
*/
public void addSame(int i, int j) {
addOrClause(i, false, j, true); // ¬x_i OR x_j
addOrClause(i, true, j, false); // x_i OR ¬x_j
}
/**
* 添加约束: x_i 和 x_j 必须不同
* 即: (x_i AND ¬x_j) OR (¬x_i AND x_j)
* 分解为: (¬x_i OR ¬x_j) AND (x_i OR x_j)
*/
public void addDifferent(int i, int j) {
addOrClause(i, false, j, false); // ¬x_i OR ¬x_j
addOrClause(i, true, j, true); // x_i OR x_j
}
private void addImplication(int from, int to) {
graph[from].add(to);
revGraph[to].add(from);
}
/**
* 使用Tarjan算法求强连通分量
*/
private void tarjan() {
dfn = new int[size];
low = new int[size];
sccId = new int[size];
inStack = new boolean[size];
stack = new ArrayDeque<>();
timestamp = 0;
sccCount = 0;
Arrays.fill(dfn, -1);
Arrays.fill(sccId, -1);
for (int i = 0; i < size; i++) {
if (dfn[i] == -1) {
dfs(i);
}
}
}
private void dfs(int u) {
dfn[u] = low[u] = ++timestamp;
stack.push(u);
inStack[u] = true;
for (int v : graph[u]) {
if (dfn[v] == -1) {
dfs(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
while (true) {
int x = stack.pop();
inStack[x] = false;
sccId[x] = sccCount;
if (x == u) break;
}
sccCount++;
}
}
/**
* 求解2-SAT问题
* @return 若可满足，返回各变量的赋值；若不可满足，返回null
*/
public boolean[] solve() {
tarjan();
// 检查每个变量的正负节点是否在同一SCC
boolean[] assignment = new boolean[n];
for (int i = 0; i < n; i++) {
if (sccId[varTrue(i)] == sccId[varFalse(i)]) {
return null; // 不可满足
}
}
// 按SCC的拓扑逆序赋值（Tarjan中sccId大的先出栈，拓扑序小）
// sccId小的在拓扑序后面，应该优先赋值
// 如果 varTrue(i) 的 sccId > varFalse(i) 的 sccId，则 x_i = false
for (int i = 0; i < n; i++) {
assignment[i] = sccId[varTrue(i)] > sccId[varFalse(i)];
}
return assignment;
}
/**
* 验证解的正确性
*/
public boolean verify(boolean[] assignment) {
// 简单验证: 检查每条边的蕴含关系是否满足
for (int u = 0; u < size; u++) {
boolean uVal = getValue(u, assignment);
for (int v : graph[u]) {
boolean vVal = getValue(v, assignment);
// u -> v 意味着 如果u为真则v必须为真
if (uVal && !vVal) {
return false;
}
}
}
return true;
}
private boolean getValue(int node, boolean[] assignment) {
if (node < n) {
return assignment[node]; // x_i
} else {
return !assignment[node - n]; // ¬x_i
}
}
public static void main(String[] args) {
// 示例1: 可满足
System.out.println("========== 示例1: 会议安排 ==========");
TwoSAT solver1 = new TwoSAT(3);
// 会议0和1不能同时在上午
solver1.addNotBothTrue(0, 1);
// 会议1和2不能同时在下午
solver1.addNotBothFalse(1, 2);
// 会议0和2必须在同一时段
solver1.addSame(0, 2);
boolean[] sol1 = solver1.solve();
printSolution(sol1, 3);
// 示例2: 不可满足
System.out.println("\n========== 示例2: 矛盾约束 ==========");
TwoSAT solver2 = new TwoSAT(2);
// x0 OR x1
solver2.addOrClause(0, true, 1, true);
// ¬x0 OR ¬x1
solver2.addOrClause(0, false, 1, false);
// x0 OR ¬x1
solver2.addOrClause(0, true, 1, false);
// ¬x0 OR x1
solver2.addOrClause(0, false, 1, true);
// 以上四个约束要求: x0 != x1 且 x0 == x1，矛盾！
boolean[] sol2 = solver2.solve();
printSolution(sol2, 2);
// 示例3: 复杂可满足问题
System.out.println("\n========== 示例3: 5变量约束系统 ==========");
TwoSAT solver3 = new TwoSAT(5);
solver3.addOrClause(0, true, 1, false); // x0 OR ¬x1
solver3.addOrClause(1, true, 2, true); // x1 OR x2
solver3.addOrClause(2, false, 3, true); // ¬x2 OR x3
solver3.addOrClause(3, false, 4, false); // ¬x3 OR ¬x4
solver3.addOrClause(0, false, 4, true); // ¬x0 OR x4
solver3.addNotBothTrue(1, 3); // ¬x1 OR ¬x3
boolean[] sol3 = solver3.solve();
printSolution(sol3, 5);
if (sol3 != null) {
System.out.println("验证结果: " + solver3.verify(sol3));
}
}
private static void printSolution(boolean[] sol, int n) {
if (sol == null) {
System.out.println("结果: 不可满足 (UNSAT)");
} else {
System.out.println("结果: 可满足 (SAT)");
System.out.print("赋值: ");
for (int i = 0; i < n; i++) {
System.out.printf("x%d=%s ", i, sol[i] ? "T" : "F");
}
System.out.println();
}
}
}
四、应用场景：图着色判定
2-SAT可以判定一个图是否能用两种颜色着色（二分图判定的高级版本）。
/**
* 使用2-SAT解决二分图判定问题
* 实际上是2-SAT的一个简单应用
*/
public class BipartiteWith2SAT {
/**
* 判定图是否为二分图，使用2-SAT建模
* 每个节点u: x_u = true表示染红色, false表示染蓝色
* 边(u,v)约束: x_u != x_v，即 (¬x_u OR ¬x_v) AND (x_u OR x_v)
*/
public static boolean isBipartite(int n, int[][] edges) {
TwoSAT solver = new TwoSAT(n);
for (int[] e : edges) {
int u = e[0], v = e[1];
solver.addDifferent(u, v); // x_u != x_v
}
return solver.solve() != null;
}
public static void main(String[] args) {
// 二分图示例
int[][] edges1 = {{0,1}, {1,2}, {2,3}, {3,0}}; // 偶环，是二分图
System.out.println("图1(偶环)是二分图: " + isBipartite(4, edges1));
// 非二分图示例
int[][] edges2 = {{0,1}, {1,2}, {2,0}}; // 奇环，不是二分图
System.out.println("图2(奇环)是二分图: " + isBipartite(3, edges2));
}
}
五、复杂度分析
| 步骤 | 时间复杂度 | 空间复杂度 |
|---|---|---|
| 建图 | O(n + m) | O(n + m) |
| Tarjan求SCC | O(n + m) | O(n) |
| 检查与赋值 | O(n) | O(n) |
| 总计 | O(n + m) | O(n + m) |
其中 n 为变量数，m 为子句数。每个子句产生2条边。
六、与3-SAT的对比
| 问题 | 时间复杂度 | 可解性 |
|---|---|---|
| 2-SAT | O(n + m)，多项式时间 | P问题，有高效算法 |
| 3-SAT | 无已知多项式算法 | NP完全问题 |
2-SAT之所以可高效求解，关键在于每个子句只有两个文字，使得蕴含图具有特殊结构。3-SAT及以上的SAT问题是NP完全的，只能使用指数级算法（如DPLL）求解。
七、总结
2-SAT是连接布尔逻辑与图论算法的璀璨明珠。通过将”或”子句转化为”蕴含”关系，再借助强连通分量判断矛盾，我们获得了一个线性时间的高效求解器。掌握2-SAT不仅能解决会议安排、图着色等经典问题，更重要的是培养了”逻辑约束转图论建模”的核心算法思维——这种转化能力在解决复杂约束满足问题时至关重要。
