数独（Sudoku）是一种经典的逻辑填数游戏，玩家需要在9×9的格子中填入数字1-9，使得每行、每列以及每个3×3宫格内的数字均不重复。本文将介绍如何将数独问题转化为布尔可满足性问题（SAT），并使用DPLL算法进行高效求解。
问题建模：从数独到SAT
SAT问题是判定一个布尔公式是否存在满足赋值的问题。将数独转化为SAT的核心思想是：为每个格子(i,j)和每个可能的数字k定义一个布尔变量x(i,j,k)，当且仅当格子(i,j)填入数字k时，x(i,j,k)为真。
约束条件的CNF表示
数独规则可以编码为合取范式（CNF）：
- 每个格子至少填一个数字：对于每个格子(i,j)，至少有一个x(i,j,k)为真
- 每个格子至多填一个数字：对于每个格子(i,j)，不能同时有两个不同的数字
- 每行数字不重复：每行中每个数字k只能出现一次
- 每列数字不重复：每列中每个数字k只能出现一次
- 每个宫格数字不重复：每个3×3宫格中每个数字k只能出现一次
DPLL算法核心思想
DPLL（Davis-Putnam-Logemann-Loveland）算法是求解SAT问题的经典回溯算法，核心策略包括：
- 单元传播（Unit Propagation）：如果子句中只剩一个未赋值文字，则该文字必须为真
- 纯文字消除（Pure Literal Elimination）：如果一个变量在所有子句中只以正或负形式出现，则可以直接赋值
- 回溯搜索（Backtracking）：对未赋值变量尝试真/假赋值，递归求解
Java实现
import java.util.*;
/**
* SAT求解器：使用DPLL算法解决数独问题
* 将数独转化为CNF布尔公式，通过单元传播和回溯搜索找到满足解
*/
public class SudokuDPLL {
// 数独大小
private static final int N = 9;
private static final int BOX = 3;
// CNF公式：子句列表，每个子句是文字列表（正数表示正文字，负数表示负文字）
private List<List<Integer>> clauses;
// 变量赋值状态：0=未赋值, 1=真, -1=假
private int[] assignment;
// 变量总数：N*N*N = 729个布尔变量
private int varCount;
public SudokuDPLL() {
this.clauses = new ArrayList<>();
this.varCount = N * N * N;
this.assignment = new int[varCount + 1];
}
/**
* 将数独坐标和数字编码为变量编号
* 变量编号 = (row * N + col) * N + (num - 1) + 1
*/
private int var(int row, int col, int num) {
return (row * N + col) * N + (num - 1) + 1;
}
/**
* 添加一个子句到CNF公式
*/
private void addClause(List<Integer> clause) {
clauses.add(new ArrayList<>(clause));
}
/**
* 构建数独的CNF约束
* 生成所有必要的子句确保数独规则被满足
*/
public void buildCNF(int[][] puzzle) {
clauses.clear();
// 1. 每个格子至少填一个数字
for (int r = 0; r < N; r++) {
for (int c = 0; c < N; c++) {
List<Integer> clause = new ArrayList<>();
for (int n = 1; n <= N; n++) {
clause.add(var(r, c, n));
}
addClause(clause);
}
}
// 2. 每个格子至多填一个数字（两两互斥）
for (int r = 0; r < N; r++) {
for (int c = 0; c < N; c++) {
for (int n1 = 1; n1 <= N; n1++) {
for (int n2 = n1 + 1; n2 <= N; n2++) {
List<Integer> clause = new ArrayList<>();
clause.add(-var(r, c, n1));
clause.add(-var(r, c, n2));
addClause(clause);
}
}
}
}
// 3. 每行数字不重复
for (int r = 0; r < N; r++) {
for (int n = 1; n <= N; n++) {
for (int c1 = 0; c1 < N; c1++) {
for (int c2 = c1 + 1; c2 < N; c2++) {
List<Integer> clause = new ArrayList<>();
clause.add(-var(r, c1, n));
clause.add(-var(r, c2, n));
addClause(clause);
}
}
}
}
// 4. 每列数字不重复
for (int c = 0; c < N; c++) {
for (int n = 1; n <= N; n++) {
for (int r1 = 0; r1 < N; r1++) {
for (int r2 = r1 + 1; r2 < N; r2++) {
List<Integer> clause = new ArrayList<>();
clause.add(-var(r1, c, n));
clause.add(-var(r2, c, n));
addClause(clause);
}
}
}
}
// 5. 每个宫格数字不重复
for (int br = 0; br < BOX; br++) {
for (int bc = 0; bc < BOX; bc++) {
for (int n = 1; n <= N; n++) {
for (int i = 0; i < N; i++) {
int r1 = br * BOX + i / BOX;
int c1 = bc * BOX + i % BOX;
for (int j = i + 1; j < N; j++) {
int r2 = br * BOX + j / BOX;
int c2 = bc * BOX + j % BOX;
List<Integer> clause = new ArrayList<>();
clause.add(-var(r1, c1, n));
clause.add(-var(r2, c2, n));
addClause(clause);
}
}
}
}
}
// 6. 已填数字的单元子句（强制约束）
for (int r = 0; r < N; r++) {
for (int c = 0; c < N; c++) {
if (puzzle[r][c] != 0) {
List<Integer> clause = new ArrayList<>();
clause.add(var(r, c, puzzle[r][c]));
addClause(clause);
}
}
}
}
/**
* DPLL核心求解算法
* 结合单元传播和回溯搜索求解SAT问题
* @return 是否存在满足赋值
*/
public boolean solve() {
Arrays.fill(assignment, 0);
return dpll(new ArrayList<>(clauses));
}
/**
* DPLL递归求解
* @param currentClauses 当前子句集合
* @return 是否存在满足赋值
*/
private boolean dpll(List<List<Integer>> currentClauses) {
// 应用单元传播直到无法继续
boolean changed;
do {
changed = false;
Iterator<List<Integer>> it = currentClauses.iterator();
while (it.hasNext()) {
List<Integer> clause = it.next();
// 简化子句：移除已满足的文字和已赋值为假的文字
List<Integer> simplified = simplifyClause(clause);
if (simplified == null) {
// 子句已被满足
it.remove();
changed = true;
} else if (simplified.isEmpty()) {
// 空子句，冲突
return false;
} else if (simplified.size() == 1) {
// 单元子句，强制赋值
int lit = simplified.get(0);
int var = Math.abs(lit);
int val = lit > 0 ? 1 : -1;
if (assignment[var] == -val) {
return false; // 冲突
}
if (assignment[var] == 0) {
assignment[var] = val;
changed = true;
}
it.remove();
}
}
} while (changed);
// 检查是否所有子句都被满足
if (currentClauses.isEmpty()) {
return true;
}
// 选择未赋值变量进行分支（使用MOMS启发式：选择出现在最短子句中最频繁的变量）
int branchVar = selectVariable(currentClauses);
if (branchVar == 0) {
return true;
}
// 保存当前赋值状态以便回溯
int[] savedAssignment = assignment.clone();
// 尝试赋值为真
assignment[branchVar] = 1;
List<List<Integer>> clausesCopy = copyClauses(currentClauses);
if (dpll(clausesCopy)) {
return true;
}
// 回溯，尝试赋值为假
assignment = savedAssignment;
assignment[branchVar] = -1;
clausesCopy = copyClauses(currentClauses);
return dpll(clausesCopy);
}
/**
* 简化子句：根据当前赋值状态
* @return null表示子句已被满足，空列表表示空子句（冲突），否则返回简化后的子句
*/
private List<Integer> simplifyClause(List<Integer> clause) {
List<Integer> result = new ArrayList<>();
for (int lit : clause) {
int var = Math.abs(lit);
int val = assignment[var];
if (val == 0) {
result.add(lit);
} else if ((lit > 0 && val == 1) || (lit < 0 && val == -1)) {
return null; // 子句已被满足
}
// 否则该文字为假，跳过
}
return result;
}
/**
* 复制子句列表
*/
private List<List<Integer>> copyClauses(List<List<Integer>> clauses) {
List<List<Integer>> copy = new ArrayList<>();
for (List<Integer> clause : clauses) {
copy.add(new ArrayList<>(clause));
}
return copy;
}
/**
* 选择分支变量：选择第一个未赋值变量
*/
private int selectVariable(List<List<Integer>> clauses) {
for (List<Integer> clause : clauses) {
for (int lit : clause) {
int var = Math.abs(lit);
if (assignment[var] == 0) {
return var;
}
}
}
return 0;
}
/**
* 将求解结果转换回数独矩阵
*/
public int[][] getSolution() {
int[][] solution = new int[N][N];
for (int r = 0; r < N; r++) {
for (int c = 0; c < N; c++) {
for (int n = 1; n <= N; n++) {
if (assignment[var(r, c, n)] == 1) {
solution[r][c] = n;
break;
}
}
}
}
return solution;
}
/**
* 打印数独矩阵
*/
public void printGrid(int[][] grid) {
for (int r = 0; r < N; r++) {
if (r % BOX == 0 && r != 0) {
System.out.println("------+-------+------");
}
for (int c = 0; c < N; c++) {
if (c % BOX == 0 && c != 0) {
System.out.print("| ");
}
System.out.print(grid[r][c] == 0 ? ". " : grid[r][c] + " ");
}
System.out.println();
}
}
public static void main(String[] args) {
// 测试数独谜题（0表示空格）
int[][] puzzle = {
{5, 3, 0, 0, 7, 0, 0, 0, 0},
{6, 0, 0, 1, 9, 5, 0, 0, 0},
{0, 9, 8, 0, 0, 0, 0, 6, 0},
{8, 0, 0, 0, 6, 0, 0, 0, 3},
{4, 0, 0, 8, 0, 3, 0, 0, 1},
{7, 0, 0, 0, 2, 0, 0, 0, 6},
{0, 6, 0, 0, 0, 0, 2, 8, 0},
{0, 0, 0, 4, 1, 9, 0, 0, 5},
{0, 0, 0, 0, 8, 0, 0, 7, 9}
};
SudokuDPLL solver = new SudokuDPLL();
System.out.println("原始数独：");
solver.printGrid(puzzle);
System.out.println();
long start = System.currentTimeMillis();
solver.buildCNF(puzzle);
System.out.println("CNF子句数量：" + solver.clauses.size());
if (solver.solve()) {
long end = System.currentTimeMillis();
int[][] solution = solver.getSolution();
System.out.println("求解结果：");
solver.printGrid(solution);
System.out.println("\n求解耗时：" + (end - start) + "ms");
} else {
System.out.println("该数独无解！");
}
}
}
算法复杂度分析
DPLL算法的最坏时间复杂度为O(2^n)，其中n是变量数量。对于数独问题，有729个变量，直接穷举不可行。但得益于单元传播和约束传播，实际求解效率远高于穷举。
对于标准9×9数独，DPLL求解器通常能在毫秒级别完成求解。CNF子句数量约为11745个，包括单元子句、二元子句等。
总结
本文将数独问题转化为SAT问题，使用DPLL算法进行求解。通过CNF编码将数独的约束条件转化为布尔公式，利用单元传播减少搜索空间，通过回溯搜索找到满足解。这种方法展示了如何将组合优化问题转化为逻辑问题，并利用高效的SAT求解技术进行求解。
