引言
约束满足问题（Constraint Satisfaction Problem, CSP）是人工智能和运筹学中的核心问题类型。从数独、填字游戏到电路设计验证，CSP的形式化框架能够统一描述这些看似不同的问题。命题逻辑约束满足是最基础的CSP形式，它将问题转化为布尔变量的合取范式（CNF），通过系统化的搜索寻找满足所有约束的赋值。
本文将用Java构建一个通用的回溯求解框架，支持单元传播（Unit Propagation）和纯文字消除（Pure Literal Elimination）等优化技术，并以经典的逻辑谜题为例展示其威力。
算法原理
命题逻辑基础
合取范式（CNF）是由若干子句（clause）的合取（AND）构成的公式，每个子句是若干文字（literal）的析取（OR）。例如：
$$(x_1 \lor \neg x_2) \land (\neg x_1 \lor x_3 \lor x_4) \land (x_2 \lor \neg x_3)$$
DPLL算法（Davis-Putnam-Logemann-Loveland）是求解SAT问题的经典回溯算法：
- 单元传播：如果某个子句只剩一个未赋值的文字，则该文字必须为真
- 纯文字消除：如果某个变量在所有子句中只以正或只以负形式出现，可直接赋值
- 分支选择：选择一个未赋值变量，分别尝试赋值为真/假，递归求解
- 冲突回溯：如果某分支导致矛盾，回溯到上一决策点尝试另一分支
回溯框架设计
function DPLL(formula, assignment):
formula = UnitPropagate(formula, assignment)
formula = PureLiteralEliminate(formula, assignment)
if formula has empty clause: return UNSAT
if formula has no clauses: return SAT
var = ChooseUnassignedVariable(formula)
if DPLL(formula ∧ var, assignment ∪ {var=true}): return SAT
if DPLL(formula ∧ ¬var, assignment ∪ {var=false}): return SAT
return UNSAT
Java实现
import java.util.*;
/**
* 命题逻辑SAT求解器：基于DPLL算法的回溯框架
* 支持单元传播和纯文字消除优化
*/
public class DPLLSolver {
/**
* 文字：带符号的变量
* 正数表示正文字，负数表示负文字
*/
static class Literal {
int var; // 变量编号（从1开始）
boolean positive;
Literal(int var, boolean positive) {
this.var = var;
this.positive = positive;
}
int toInt() {
return positive ? var : -var;
}
Literal negate() {
return new Literal(var, !positive);
}
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (!(o instanceof Literal)) return false;
Literal other = (Literal) o;
return var == other.var && positive == other.positive;
}
@Override
public int hashCode() {
return Objects.hash(var, positive);
}
@Override
public String toString() {
return positive ? "x" + var : "¬x" + var;
}
}
/**
* 子句：文字的析取
*/
static class Clause {
Set<Literal> literals = new HashSet<>();
Clause(Collection<Literal> lits) {
literals.addAll(lits);
}
Clause(Clause other) {
literals.addAll(other.literals);
}
boolean isEmpty() {
return literals.isEmpty();
}
boolean isUnit() {
return literals.size() == 1;
}
Literal getUnitLiteral() {
return literals.iterator().next();
}
@Override
public String toString() {
if (literals.isEmpty()) return "⊥";
return "(" + String.join(" ∨ ",
literals.stream().map(Literal::toString).toArray(String[]::new)) + ")";
}
}
/**
* CNF公式：子句的合取
*/
static class CNF {
List<Clause> clauses = new ArrayList<>();
int numVars = 0;
CNF() {}
CNF(CNF other) {
for (Clause c : other.clauses) {
clauses.add(new Clause(c));
}
numVars = other.numVars;
}
void addClause(Clause c) {
clauses.add(c);
for (Literal l : c.literals) {
numVars = Math.max(numVars, l.var);
}
}
boolean hasEmptyClause() {
return clauses.stream().anyMatch(Clause::isEmpty);
}
boolean isEmpty() {
return clauses.isEmpty();
}
@Override
public String toString() {
if (clauses.isEmpty()) return "⊤";
return String.join(" ∧ ",
clauses.stream().map(Clause::toString).toArray(String[]::new));
}
}
private int decisionCount = 0;
private int propagationCount = 0;
/**
* 单元传播：强制满足单子句
* 如果子句只剩一个未赋值文字，则该文字必须为真
*/
public CNF unitPropagate(CNF formula, Map<Integer, Boolean> assignment) {
boolean changed;
CNF result = new CNF(formula);
do {
changed = false;
List<Clause> toRemove = new ArrayList<>();
for (Clause clause : result.clauses) {
// 收集未赋值文字
List<Literal> unassigned = new ArrayList<>();
boolean satisfied = false;
for (Literal lit : clause.literals) {
if (!assignment.containsKey(lit.var)) {
unassigned.add(lit);
} else if (assignment.get(lit.var) == lit.positive) {
satisfied = true;
break;
}
}
if (satisfied) {
toRemove.add(clause);
} else if (unassigned.isEmpty()) {
// 所有文字都被赋值且都不满足 → 空子句（冲突）
return new CNF(); // 返回空公式表示冲突
} else if (unassigned.size() == 1) {
// 单子句：强制赋值
Literal unit = unassigned.get(0);
assignment.put(unit.var, unit.positive);
propagationCount++;
changed = true;
}
}
result.clauses.removeAll(toRemove);
// 重新过滤已满足的子句
if (changed) {
result.clauses.removeIf(c -> {
for (Literal lit : c.literals) {
if (assignment.containsKey(lit.var) &&
assignment.get(lit.var) == lit.positive) {
return true;
}
}
return false;
});
}
} while (changed);
return result;
}
/**
* 纯文字消除：如果变量只以单一极性出现，可直接赋值
*/
public CNF pureLiteralEliminate(CNF formula, Map<Integer, Boolean> assignment) {
Map<Integer, Boolean> polarity = new HashMap<>();
for (Clause clause : formula.clauses) {
for (Literal lit : clause.literals) {
if (assignment.containsKey(lit.var)) continue;
if (!polarity.containsKey(lit.var)) {
polarity.put(lit.var, lit.positive);
} else if (polarity.get(lit.var) != lit.positive) {
polarity.put(lit.var, null); // 混合极性
}
}
}
CNF result = new CNF(formula);
for (Map.Entry<Integer, Boolean> entry : polarity.entrySet()) {
if (entry.getValue() != null) {
assignment.put(entry.getKey(), entry.getValue());
// 移除包含该纯文字的子句
result.clauses.removeIf(c -> c.literals.stream()
.anyMatch(l -> l.var == entry.getKey() && l.positive == entry.getValue()));
}
}
return result;
}
/**
* DPLL核心算法
*/
public boolean solve(CNF formula, Map<Integer, Boolean> assignment) {
// 应用单元传播
formula = unitPropagate(formula, assignment);
if (formula == null || formula.clauses == null) return false; // 冲突
// 应用纯文字消除
formula = pureLiteralEliminate(formula, assignment);
// 检查终止条件
if (formula.hasEmptyClause()) return false; // UNSAT
if (formula.isEmpty()) return true; // SAT
// 选择分支变量（启发式：选择出现次数最多的变量）
int branchVar = chooseVariable(formula, assignment);
if (branchVar == -1) return true;
decisionCount++;
// 尝试赋值为true
Map<Integer, Boolean> copy1 = new HashMap<>(assignment);
copy1.put(branchVar, true);
if (solve(new CNF(formula), copy1)) {
assignment.putAll(copy1);
return true;
}
// 尝试赋值为false
Map<Integer, Boolean> copy2 = new HashMap<>(assignment);
copy2.put(branchVar, false);
if (solve(new CNF(formula), copy2)) {
assignment.putAll(copy2);
return true;
}
return false;
}
/**
* 选择下一个分支变量（MOM启发式：最大出现次数）
*/
private int chooseVariable(CNF formula, Map<Integer, Boolean> assignment) {
Map<Integer, Integer> frequency = new HashMap<>();
for (Clause clause : formula.clauses) {
if (clause.literals.size() <= 2) { // 优先从短子句中选择
for (Literal lit : clause.literals) {
if (!assignment.containsKey(lit.var)) {
frequency.merge(lit.var, 1, Integer::sum);
}
}
}
}
if (frequency.isEmpty()) {
for (Clause clause : formula.clauses) {
for (Literal lit : clause.literals) {
if (!assignment.containsKey(lit.var)) {
return lit.var;
}
}
}
return -1;
}
return Collections.max(frequency.entrySet(), Map.Entry.comparingByValue()).getKey();
}
// ==================== 逻辑谜题建模示例 ====================
/**
* 构造一个简单的逻辑谜题：
* 三人A、B、C中有一人说真话，两人说假话。
* A说："B在说谎"
* B说："C在说谎"
* C说："A和B都在说谎"
* 谁是说真话的人？
*/
public static CNF buildTruthTellerPuzzle() {
CNF cnf = new CNF();
// x1=A说真话, x2=B说真话, x3=C说真话
// 恰好一个说真话：至少一个 ∧ 至多一个
// 至少一个
cnf.addClause(new Clause(Arrays.asList(
new Literal(1, true), new Literal(2, true), new Literal(3, true))));
// 至多一个：(¬x1 ∨ ¬x2) ∧ (¬x1 ∨ ¬x3) ∧ (¬x2 ∨ ¬x3)
cnf.addClause(new Clause(Arrays.asList(new Literal(1, false), new Literal(2, false))));
cnf.addClause(new Clause(Arrays.asList(new Literal(1, false), new Literal(3, false))));
cnf.addClause(new Clause(Arrays.asList(new Literal(2, false), new Literal(3, false))));
// A说"B在说谎"：x1 → ¬x2，即 ¬x1 ∨ ¬x2
cnf.addClause(new Clause(Arrays.asList(new Literal(1, false), new Literal(2, false))));
// B说"C在说谎"：x2 → ¬x3，即 ¬x2 ∨ ¬x3
cnf.addClause(new Clause(Arrays.asList(new Literal(2, false), new Literal(3, false))));
// C说"A和B都在说谎"：x3 → (¬x1 ∧ ¬x2)，即 (¬x3 ∨ ¬x1) ∧ (¬x3 ∨ ¬x2)
cnf.addClause(new Clause(Arrays.asList(new Literal(3, false), new Literal(1, false))));
cnf.addClause(new Clause(Arrays.asList(new Literal(3, false), new Literal(2, false))));
return cnf;
}
/**
* 构造2x2数独约束（简化版）
*/
public static CNF buildMiniSudoku() {
CNF cnf = new CNF();
// x_ij_k 表示格子(i,j)填数字k
// 简化：用1-4表示2x2数独的四个格子，每个格子一个变量
// 实际数独约束较复杂，这里展示框架能力
// 每个格子至少一个数字
for (int i = 1; i <= 2; i++) {
for (int j = 1; j <= 2; j++) {
List<Literal> atLeastOne = new ArrayList<>();
for (int k = 1; k <= 2; k++) {
int var = (i-1)*4 + (j-1)*2 + k;
atLeastOne.add(new Literal(var, true));
}
cnf.addClause(new Clause(atLeastOne));
}
}
return cnf;
}
public static void main(String[] args) {
// 测试1：逻辑谜题
System.out.println("=== 逻辑谜题求解：谁在说真话？ ===");
CNF puzzle = buildTruthTellerPuzzle();
System.out.println("CNF公式: " + puzzle);
DPLLSolver solver = new DPLLSolver();
Map<Integer, Boolean> assignment = new HashMap<>();
boolean sat = solver.solve(puzzle, assignment);
System.out.println("可满足性: " + (sat ? "SAT" : "UNSAT"));
if (sat) {
System.out.println("解: " + assignment);
System.out.println("A说真话: " + assignment.get(1));
System.out.println("B说真话: " + assignment.get(2));
System.out.println("C说真话: " + assignment.get(3));
}
System.out.println("决策次数: " + solver.decisionCount);
System.out.println("传播次数: " + solver.propagationCount);
// 测试2：简单SAT实例
System.out.println("\n=== 简单SAT测试 ===");
CNF simple = new CNF();
simple.addClause(new Clause(Arrays.asList(new Literal(1, true), new Literal(2, true))));
simple.addClause(new Clause(Arrays.asList(new Literal(1, false), new Literal(2, true))));
simple.addClause(new Clause(Arrays.asList(new Literal(1, false), new Literal(2, false))));
solver = new DPLLSolver();
assignment = new HashMap<>();
sat = solver.solve(simple, assignment);
System.out.println("公式: (x1 ∨ x2) ∧ (¬x1 ∨ x2) ∧ (¬x1 ∨ ¬x2)");
System.out.println("可满足性: " + (sat ? "SAT" : "UNSAT"));
if (sat) System.out.println("解: " + assignment);
}
}
算法分析
时间复杂度
DPLL算法在最坏情况下需要遍历 $2^n$ 个赋值空间，时间复杂度为 $O(2^n)$。但通过单元传播和纯文字消除，实际运行中常大幅剪枝。
现代SAT求解器（如MiniSat、Glucose）在DPLL基础上增加了：
– 冲突驱动子句学习（CDCL）：从冲突中学习新的子句
– 变量状态独立衰减和（VSIDS）启发式：动态调整变量优先级
– 重启策略：定期重置搜索状态
这些优化使得现代求解器可以处理数百万变量的问题。
空间复杂度
基础DPLL的空间复杂度为 $O(n + m)$，其中 $n$ 是变量数，$m$ 是子句数。CDCL版本需要额外空间存储学习子句。
完备性与正确性
DPLL算法是可靠且完备的：
– 可靠性：如果算法返回SAT，则确实存在满足赋值
– 完备性：如果公式可满足，算法一定能在有限步内找到解（或证明UNSAT）
扩展应用
数独求解
标准9×9数独可以编码为约729个变量和数千个子句的SAT问题。使用高效的SAT求解器，即使在最坏情况下也能在毫秒级求解。
电路验证
硬件设计中的等价性检验、死锁检测都可以转化为SAT问题。Intel和AMD的处理器设计流程中，SAT求解器是不可或缺的验证工具。
规划与调度
AI规划问题（如动作序列规划）和工厂作业调度都可以通过CSP/SAT框架求解，利用约束传播大幅缩减搜索空间。
总结
本文实现了一个基于DPLL算法的通用命题逻辑SAT求解器，支持单元传播和纯文字消除等核心优化。从逻辑谜题到数独、从电路验证到AI规划，约束满足框架展现了强大的问题建模能力。理解DPLL的回溯搜索机制，不仅是掌握SAT求解的基础，更是理解AI中搜索与推理本质的关键一步。在实际工程中，建议将自定义求解器作为学习工具，生产环境应使用经过高度优化的工业级求解器如MiniSat或Z3。
