每日算法 — 使用java实现扫雷：SAT求解器转化与DPLL回溯搜索

扫雷（Minesweeper）是Windows系统自带的经典逻辑推理游戏。玩家需要根据已揭示数字格周围的地雷分布信息，通过纯逻辑推理确定未揭示格子的安全性。本文用Java实现一个带AI求解能力的扫雷引擎，核心讲解如何将扫雷约束转化为布尔可满足性问题（SAT），以及经典DPLL回溯搜索算法如何通过单位传播和纯文字消除高效求解命题逻辑公式。

一、扫雷规则与逻辑建模

1.1 为什么扫雷是NP完全问题

扫雷的判定问题（给定部分揭示的盘面，判断是否存在一种地雷排布满足所有已揭示数字）被证明是NP完全的。这意味着：当盘面足够大时，不存在已知的多项式时间算法能求解所有情况。然而，许多实际盘面中的约束具有特殊结构，可以通过高效的SAT求解技术快速处理。

1.2 核心数据结构定义

我们用以下类对扫雷世界进行建模：每个格子有三种状态——未揭示、已揭示（显示数字0-8）、已标记为地雷。Board类记录整个盘面，Constraint类表示一个已揭示数字格对其邻域施加的约束。

import java.util.*;

/**
 * 格子状态枚举
 * COVERED: 未揭示
 * REVEALED: 已揭示，显示周围地雷数
 * FLAGGED: 已被玩家标记为地雷
 */
enum CellState {
    COVERED, REVEALED, FLAGGED
}

/**
 * 单个格子
 * 若状态为REVEALED，value存储周围8邻域的地雷总数（0-8）
 * 若状态为COVERED或FLAGGED，value无意义
 */
class Cell {
    CellState state = CellState.COVERED;
    int value = 0; // 周围地雷数，仅在REVEALED时有效
    boolean isMine = false; // 真实是否为地雷（仅游戏生成时设置）
}

/**
 * 扫雷盘面
 * 使用二维数组存储格子，提供邻居遍历、约束提取等方法
 */
class Board {
    final int rows;
    final int cols;
    final int totalMines;
    final Cell[][] grid;
    int remainingMines; // 剩余待标记地雷数
    boolean gameOver = false;
    boolean win = false;

    Board(int rows, int cols, int mines) {
        this.rows = rows;
        this.cols = cols;
        this.totalMines = mines;
        this.remainingMines = mines;
        this.grid = new Cell[rows][cols];
        for (int r = 0; r < rows; r++)
            for (int c = 0; c < cols; c++)
                grid[r][c] = new Cell();
        placeMines();
        computeNumbers();
    }

    /**
     * 随机放置地雷，确保第一次点击不会踩雷由外部逻辑保证
     */
    private void placeMines() {
        Random rand = new Random();
        int placed = 0;
        while (placed < totalMines) {
            int r = rand.nextInt(rows);
            int c = rand.nextInt(cols);
            if (!grid[r][c].isMine) {
                grid[r][c].isMine = true;
                placed++;
            }
        }
    }

    /**
     * 计算每个非地雷格子的周围地雷数
     */
    private void computeNumbers() {
        for (int r = 0; r < rows; r++) {
            for (int c = 0; c < cols; c++) {
                if (grid[r][c].isMine) continue;
                int count = 0;
                for (int[] n : neighbors(r, c))
                    if (grid[n[0]][n[1]].isMine) count++;
                grid[r][c].value = count;
            }
        }
    }

    /**
     * 获取指定格子的8邻域坐标列表
     */
    List<int[]> neighbors(int r, int c) {
        List<int[]> list = new ArrayList<>();
        for (int dr = -1; dr <= 1; dr++) {
            for (int dc = -1; dc <= 1; dc++) {
                if (dr == 0 && dc == 0) continue;
                int nr = r + dr, nc = c + dc;
                if (nr >= 0 && nr < rows && nc >= 0 && nc < cols)
                    list.add(new int[]{nr, nc});
            }
        }
        return list;
    }

    /**
     * 揭示指定格子
     * @return false 表示踩到地雷，游戏结束
     */
    boolean reveal(int r, int c) {
        Cell cell = grid[r][c];
        if (cell.state != CellState.COVERED) return true;
        cell.state = CellState.REVEALED;
        if (cell.isMine) {
            gameOver = true;
            return false;
        }
        // 若值为0，自动级联揭示周围格子（BFS展开）
        if (cell.value == 0) {
            Queue<int[]> q = new LinkedList<>();
            q.offer(new int[]{r, c});
            while (!q.isEmpty()) {
                int[] cur = q.poll();
                for (int[] n : neighbors(cur[0], cur[1])) {
                    Cell nc = grid[n[0]][n[1]];
                    if (nc.state == CellState.COVERED && !nc.isMine) {
                        nc.state = CellState.REVEALED;
                        if (nc.value == 0) q.offer(n);
                    }
                }
            }
        }
        checkWin();
        return true;
    }

    /**
     * 标记/取消标记地雷
     */
    void toggleFlag(int r, int c) {
        Cell cell = grid[r][c];
        if (cell.state == CellState.COVERED) {
            cell.state = CellState.FLAGGED;
            remainingMines--;
        } else if (cell.state == CellState.FLAGGED) {
            cell.state = CellState.COVERED;
            remainingMines++;
        }
    }

    /**
     * 检查是否获胜：所有非地雷格子均已揭示
     */
    private void checkWin() {
        int revealed = 0;
        for (int r = 0; r < rows; r++)
            for (int c = 0; c < cols; c++)
                if (grid[r][c].state == CellState.REVEALED) revealed++;
        if (revealed == rows * cols - totalMines) {
            win = true;
            gameOver = true;
        }
    }

    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder();
        sb.append("  ");
        for (int c = 0; c < cols; c++) sb.append(c % 10).append(" ");
        sb.append("\n");
        for (int r = 0; r < rows; r++) {
            sb.append(r % 10).append(" ");
            for (int c = 0; c < cols; c++) {
                Cell cell = grid[r][c];
                if (cell.state == CellState.FLAGGED) sb.append("F ");
                else if (cell.state == CellState.COVERED) sb.append("# ");
                else if (cell.isMine) sb.append("* ");
                else sb.append(cell.value).append(" ");
            }
            sb.append("\n");
        }
        return sb.toString();
    }
}

二、从扫雷到SAT：命题逻辑建模

2.1 约束提取

对于每一个已揭示的数字格，其周围未揭示且未标记的格子构成一个约束。设某数字格值为 k，其周围有 n 个未确定格子，则其中恰好有 k - 已标记数 个是地雷。

这是一个经典的精确覆盖约束，可用布尔变量表示：为每个未确定格子引入布尔变量 x_i，x_i = true 表示该格是地雷。

2.2 转化为合取范式（CNF）

合取范式（Conjunctive Normal Form, CNF）是形如 (a ∨ b) ∧ (¬c ∨ d) ... 的公式，是SAT求解器的标准输入格式。

对于约束”n 个变量中恰好有 k 个为真”，我们需要生成两组子句：

1. 至少k个为真：从 n 个中选 n-k+1 个取反，构成子句。即对于任意 n-k+1 个变量的组合，至少有一个为真。等价于：不能存在 n-k+1 个变量同时为假。
2. 至多k个为真：从 n 个中选 k+1 个，构成子句要求至少一个为假。即不能存在 k+1 个变量同时为真。

/**
 * CNF公式表示
 * 每个子句是一个整数列表，正数表示正文字，负数表示负文字
 * 例如子句 (x1 ∨ ¬x2 ∨ x3) 表示为 [1, -2, 3]
 */
class CNF {
    final int numVars; // 变量总数
    final List<List<Integer>> clauses = new ArrayList<>();

    CNF(int numVars) {
        this.numVars = numVars;
    }

    void addClause(List<Integer> clause) {
        clauses.add(new ArrayList<>(clause));
    }

    /**
     * 添加约束：vars中恰好有exactly个为真
     */
    void addExactly(List<Integer> vars, int exactly) {
        int n = vars.size();
        // 至少exactly个：所有大小为(n - exactly + 1)的子集取反
        if (exactly > 0) {
            generateCombinations(vars, n - exactly + 1, combo -> {
                List<Integer> clause = new ArrayList<>();
                for (int v : combo) clause.add(-v);
                addClause(clause);
            });
        }
        // 至多exactly个：所有大小为(exactly + 1)的子集至少一个为假
        if (exactly < n) {
            generateCombinations(vars, exactly + 1, combo -> {
                List<Integer> clause = new ArrayList<>();
                for (int v : combo) clause.add(-v);
                addClause(clause);
            });
        }
    }

    /**
     * 组合生成辅助方法
     */
    private void generateCombinations(List<Integer> vars, int k, java.util.function.Consumer<int[]> consumer) {
        int n = vars.size();
        int[] combo = new int[k];
        combine(vars, 0, n - 1, 0, k, combo, consumer);
    }

    private void combine(List<Integer> vars, int start, int end, int index, int k,
                         int[] combo, java.util.function.Consumer<int[]> consumer) {
        if (index == k) {
            consumer.accept(combo.clone());
            return;
        }
        for (int i = start; i <= end && end - i + 1 >= k - index; i++) {
            combo[index] = vars.get(i);
            combine(vars, i + 1, end, index + 1, k, combo, consumer);
        }
    }
}

2.3 变量映射

将盘面中的每个未确定格子映射到一个唯一的整数变量ID：

/**
 * 变量映射器
 * 将盘面坐标(r,c)映射到SAT变量ID（从1开始计数）
 */
class VariableMap {
    private final Map<String, Integer> coordToVar = new HashMap<>();
    private final List<int[]> varToCoord = new ArrayList<>(); // 索引0占位，变量ID从1开始

    VariableMap() {
        varToCoord.add(new int[]{-1, -1}); // 占位
    }

    int getOrCreateVar(int r, int c) {
        String key = r + "," + c;
        if (coordToVar.containsKey(key)) return coordToVar.get(key);
        int varId = coordToVar.size() + 1;
        coordToVar.put(key, varId);
        varToCoord.add(new int[]{r, c});
        return varId;
    }

    int[] getCoord(int varId) {
        return varToCoord.get(varId);
    }

    int size() {
        return coordToVar.size();
    }
}

三、DPLL算法：经典SAT求解

3.1 算法核心思想

DPLL（Davis-Putnam-Logemann-Loveland）算法是现代SAT求解器的鼻祖，核心策略包括：

1. 单位传播（Unit Propagation）：若某子句只剩一个未赋值文字且其他文字均为假，则该文字必须为真。
2. 纯文字消除（Pure Literal Elimination）：若某变量在所有子句中只以正（或负）文字出现，可直接赋值为真（或假）。
3. 回溯搜索（Backtracking）：选择某个变量进行分支赋值（先试true，失败后试false），递归求解。

/**
 * DPLL SAT求解器
 * 求解CNF公式，返回一组满足赋值（若存在）
 */
class DPLLSolver {

    /**
     * 求解结果
     */
    static class Result {
        final boolean satisfiable;
        final Map<Integer, Boolean> assignment; // 变量ID -> 真值

        Result(boolean sat, Map<Integer, Boolean> assignment) {
            this.satisfiable = sat;
            this.assignment = assignment;
        }
    }

    Result solve(CNF cnf) {
        Map<Integer, Boolean> assignment = new HashMap<>();
        List<List<Integer>> clauses = deepCopy(cnf.clauses);
        boolean sat = dpll(clauses, assignment);
        return new Result(sat, assignment);
    }

    private boolean dpll(List<List<Integer>> clauses, Map<Integer, Boolean> assignment) {
        // 简化：应用单位传播和纯文字消除直到不动点
        while (true) {
            boolean changed = false;

            // 单位传播
            Integer unit = findUnitClause(clauses, assignment);
            while (unit != null) {
                int var = Math.abs(unit);
                boolean val = unit > 0;
                assignment.put(var, val);
                if (!simplify(clauses, var, val)) return false; // 出现空子句，不可满足
                changed = true;
                unit = findUnitClause(clauses, assignment);
            }

            // 纯文字消除
            Integer pure = findPureLiteral(clauses, assignment);
            while (pure != null) {
                int var = Math.abs(pure);
                boolean val = pure > 0;
                assignment.put(var, val);
                if (!simplify(clauses, var, val)) return false;
                changed = true;
                pure = findPureLiteral(clauses, assignment);
            }

            if (!changed) break;
        }

        // 检查是否所有子句已满足
        if (clauses.isEmpty()) return true;

        // 选择分支变量（使用最简单的启发式：取第一个未赋值变量）
        int branchVar = selectVariable(clauses, assignment);

        // 分支1: 设为true
        Map<Integer, Boolean> assignCopy = new HashMap<>(assignment);
        List<List<Integer>> clausesCopy = deepCopy(clauses);
        assignCopy.put(branchVar, true);
        if (simplify(clausesCopy, branchVar, true) && dpll(clausesCopy, assignCopy)) {
            assignment.clear();
            assignment.putAll(assignCopy);
            return true;
        }

        // 分支2: 设为false
        assignCopy = new HashMap<>(assignment);
        clausesCopy = deepCopy(clauses);
        assignCopy.put(branchVar, false);
        if (simplify(clausesCopy, branchVar, false) && dpll(clausesCopy, assignCopy)) {
            assignment.clear();
            assignment.putAll(assignCopy);
            return true;
        }

        return false;
    }

    /**
     * 寻找单位子句（只剩一个未赋值文字的子句）
     */
    private Integer findUnitClause(List<List<Integer>> clauses, Map<Integer, Boolean> assignment) {
        for (List<Integer> clause : clauses) {
            Integer unassigned = null;
            boolean satisfied = false;
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (!assignment.containsKey(var)) {
                    if (unassigned == null) unassigned = lit;
                    else { unassigned = null; break; } // 多个未赋值，不是单位子句
                } else {
                    boolean val = assignment.get(var);
                    if ((lit > 0 && val) || (lit < 0 && !val)) {
                        satisfied = true;
                        break;
                    }
                }
            }
            if (!satisfied && unassigned != null) return unassigned;
        }
        return null;
    }

    /**
     * 寻找纯文字（在所有子句中只以单一极性出现的未赋值变量）
     */
    private Integer findPureLiteral(List<List<Integer>> clauses, Map<Integer, Boolean> assignment) {
        Map<Integer, Integer> polarity = new HashMap<>(); // var -> 1(仅正), -1(仅负), 0(混合)
        for (List<Integer> clause : clauses) {
            boolean satisfied = false;
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (assignment.containsKey(var)) {
                    boolean val = assignment.get(var);
                    if ((lit > 0 && val) || (lit < 0 && !val)) { satisfied = true; break; }
                } else {
                    int sign = lit > 0 ? 1 : -1;
                    Integer cur = polarity.get(var);
                    if (cur == null) polarity.put(var, sign);
                    else if (cur != sign) polarity.put(var, 0);
                }
            }
            if (satisfied) continue;
        }
        for (Map.Entry<Integer, Integer> e : polarity.entrySet()) {
            if (e.getValue() != 0) return e.getValue() * e.getKey();
        }
        return null;
    }

    /**
     * 在赋值var=val后简化子句集合
     * @return false 如果出现空子句（不可满足）
     */
    private boolean simplify(List<List<Integer>> clauses, int var, boolean val) {
        Iterator<List<Integer>> it = clauses.iterator();
        while (it.hasNext()) {
            List<Integer> clause = it.next();
            List<Integer> newClause = new ArrayList<>();
            boolean satisfied = false;
            for (int lit : clause) {
                int v = Math.abs(lit);
                if (v == var) {
                    if ((lit > 0 && val) || (lit < 0 && !val)) {
                        satisfied = true;
                        break;
                    }
                    // 否则该文字为假，跳过
                } else {
                    newClause.add(lit);
                }
            }
            if (satisfied) {
                it.remove();
            } else {
                if (newClause.isEmpty()) return false; // 空子句
                // 原地替换
                clause.clear();
                clause.addAll(newClause);
            }
        }
        return true;
    }

    private int selectVariable(List<List<Integer>> clauses, Map<Integer, Boolean> assignment) {
        for (List<Integer> clause : clauses) {
            for (int lit : clause) {
                int var = Math.abs(lit);
                if (!assignment.containsKey(var)) return var;
            }
        }
        return -1;
    }

    private List<List<Integer>> deepCopy(List<List<Integer>> clauses) {
        List<List<Integer>> copy = new ArrayList<>();
        for (List<Integer> c : clauses) copy.add(new ArrayList<>(c));
        return copy;
    }
}

四、约束构建与多解分析

4.1 从盘面提取CNF

对于当前已揭示的盘面，我们提取所有数字格的约束，转化为CNF公式。求解该公式后，若某变量在所有满足赋值中恒为真（或恒为假），则该格确定是地雷（或安全）。

/**
 * 扫雷AI求解器
 * 将盘面约束转化为SAT问题，通过DPLL求解推断确定性格子
 */
class MinesweeperSolver {
    private final Board board;
    private final VariableMap varMap;

    MinesweeperSolver(Board board) {
        this.board = board;
        this.varMap = new VariableMap();
    }

    /**
     * 分析当前盘面，返回可确定安全的格子列表和可确定是地雷的格子列表
     */
    Result analyze() {
        CNF cnf = buildCNF();
        if (cnf.size() == 0) return new Result(Collections.emptyList(), Collections.emptyList());

        List<int[]> safeCells = new ArrayList<>();
        List<int[]> mineCells = new ArrayList<>();

        DPLLSolver solver = new DPLLSolver();

        // 对每个变量，分别假设其为真/假，检查是否可满足
        for (int v = 1; v <= cnf.numVars; v++) {
            boolean canBeTrue = checkSat(cnf, v, true, solver);
            boolean canBeFalse = checkSat(cnf, v, false, solver);

            int[] coord = varMap.getCoord(v);
            if (!canBeTrue && canBeFalse) {
                safeCells.add(coord); // 只能是假 -> 安全
            } else if (canBeTrue && !canBeFalse) {
                mineCells.add(coord); // 只能是真 -> 地雷
            }
        }

        return new Result(safeCells, mineCells);
    }

    /**
     * 检查在附加约束var=val下，CNF是否可满足
     */
    private boolean checkSat(CNF original, int var, boolean val, DPLLSolver solver) {
        CNF test = new CNF(original.numVars);
        for (List<Integer> c : original.clauses) test.addClause(c);
        test.addClause(Collections.singletonList(val ? var : -var));
        return solver.solve(test).satisfiable;
    }

    /**
     * 从当前盘面构建CNF约束
     */
    private CNF buildCNF() {
        // 收集所有未揭示且未标记的边界格子（与已揭示数字相邻的COVERED格子）
        Set<String> boundary = new LinkedHashSet<>();
        for (int r = 0; r < board.rows; r++) {
            for (int c = 0; c < board.cols; c++) {
                if (board.grid[r][c].state != CellState.REVEALED) continue;
                for (int[] n : board.neighbors(r, c)) {
                    if (board.grid[n[0]][n[1]].state == CellState.COVERED)
                        boundary.add(n[0] + "," + n[1]);
                }
            }
        }

        // 为边界格子分配变量
        for (String key : boundary) {
            String[] parts = key.split(",");
            varMap.getOrCreateVar(Integer.parseInt(parts[0]), Integer.parseInt(parts[1]));
        }

        CNF cnf = new CNF(varMap.size());

        // 为每个已揭示数字格提取约束
        for (int r = 0; r < board.rows; r++) {
            for (int c = 0; c < board.cols; c++) {
                if (board.grid[r][c].state != CellState.REVEALED) continue;
                List<Integer> vars = new ArrayList<>();
                int flagged = 0;
                for (int[] n : board.neighbors(r, c)) {
                    Cell nc = board.grid[n[0]][n[1]];
                    if (nc.state == CellState.FLAGGED) flagged++;
                    else if (nc.state == CellState.COVERED) {
                        int v = varMap.getOrCreateVar(n[0], n[1]);
                        vars.add(v);
                    }
                }
                int remaining = board.grid[r][c].value - flagged;
                if (remaining < 0) continue; // 矛盾，但正常游戏不会出现
                if (vars.isEmpty()) continue;
                if (remaining == 0) {
                    // 周围未确定格子必须全为安全
                    for (int v : vars) cnf.addClause(Collections.singletonList(-v));
                } else if (remaining == vars.size()) {
                    // 周围未确定格子必须全为地雷
                    for (int v : vars) cnf.addClause(Collections.singletonList(v));
                } else {
                    cnf.addExactly(vars, remaining);
                }
            }
        }

        return cnf;
    }

    static class Result {
        final List<int[]> safeCells;
        final List<int[]> mineCells;

        Result(List<int[]> safe, List<int[]> mine) {
            this.safeCells = safe;
            this.mineCells = mine;
        }
    }
}

五、概率推理：当SAT无法唯一确定时

5.1 为什么需要概率推理

DPLL可以告诉我们哪些格子是逻辑上必然安全或必然地雷的。但在许多盘面中，某些格子的状态无法被唯一确定——存在至少一种满足赋值使其为真，也至少一种使其为假。此时需要概率估计：计算该格子为地雷的概率，选择概率最低的格子点击。

对于小规模边界约束（通常少于25个变量），我们可以通过枚举所有满足赋值精确计算概率。

/**
 * 概率推理引擎
 * 对DPLL无法确定的格子，通过枚举所有满足赋值计算精确概率
 */
class ProbabilityEngine {

    /**
     * 计算每个边界格子是地雷的概率
     * 使用DPLL递归收集所有满足赋值（适用于小规模约束）
     */
    Map<Integer, Double> computeProbabilities(CNF cnf, List<Integer> variables) {
        Map<Integer, Integer> mineCount = new HashMap<>();
        for (int v : variables) mineCount.put(v, 0);

        int[] totalModels = new int[]{0};
        collectModels(cnf, new HashMap<>(), variables, mineCount, totalModels);

        Map<Integer, Double> probs = new HashMap<>();
        for (int v : variables) {
            probs.put(v, totalModels[0] == 0 ? 0.5 : (double) mineCount.get(v) / totalModels[0]);
        }
        return probs;
    }

    private void collectModels(CNF cnf, Map<Integer, Boolean> assignment,
                               List<Integer> variables, Map<Integer, Integer> mineCount, int[] total) {
        DPLLSolver solver = new DPLLSolver();
        DPLLSolver.Result res = solver.solve(cnf);
        if (!res.satisfiable) return;

        total[0]++;
        for (int v : variables) {
            Boolean val = res.assignment.get(v);
            if (val != null && val) mineCount.put(v, mineCount.get(v) + 1);
        }

        // 阻塞当前模型，寻找下一个
        List<Integer> blockingClause = new ArrayList<>();
        for (int v : variables) {
            Boolean val = res.assignment.get(v);
            if (val != null) blockingClause.add(val ? -v : v);
        }
        if (!blockingClause.isEmpty()) {
            CNF next = new CNF(cnf.numVars);
            for (List<Integer> c : cnf.clauses) next.addClause(c);
            next.addClause(blockingClause);
            collectModels(next, new HashMap<>(), variables, mineCount, total);
        }
    }
}

六、主程序与AI自动演示

以下主程序创建一个9×9、10颗地雷的扫雷盘面，AI使用SAT+DPLL进行自动求解演示：

public class MinesweeperDemo {
    public static void main(String[] args) {
        int rows = 9, cols = 9, mines = 10;
        Board board = new Board(rows, cols, mines);
        MinesweeperSolver solver = new MinesweeperSolver(board);
        Random rand = new Random();

        // 第一步随机点击中心区域
        int firstR = rows / 2, firstC = cols / 2;
        System.out.println("=== 扫雷AI求解演示 ===");
        System.out.println("盘面大小: " + rows + "x" + cols + ", 地雷数: " + mines);
        System.out.println("第一步随机点击: (" + firstR + "," + firstC + ")");
        board.reveal(firstR, firstC);
        System.out.println(board);

        int step = 1;
        while (!board.gameOver) {
            MinesweeperSolver.Result result = solver.analyze();

            boolean moved = false;
            // 优先标记确定的地雷
            for (int[] m : result.mineCells) {
                if (board.grid[m[0]][m[1]].state == CellState.COVERED) {
                    board.toggleFlag(m[0], m[1]);
                    System.out.println("步骤" + step + ": 逻辑推断标记地雷 (" + m[0] + "," + m[1] + ")");
                    moved = true;
                    break;
                }
            }
            if (!moved) {
                // 其次点击确定安全的格子
                for (int[] s : result.safeCells) {
                    if (board.grid[s[0]][s[1]].state == CellState.COVERED) {
                        System.out.println("步骤" + step + ": 逻辑推断安全揭示 (" + s[0] + "," + s[1] + ")");
                        board.reveal(s[0], s[1]);
                        moved = true;
                        break;
                    }
                }
            }

            if (!moved) {
                // SAT无法确定，使用概率推理或随机选择
                // 简化演示：随机选择一个未揭示的非标记格子
                List<int[]> unknown = new ArrayList<>();
                for (int r = 0; r < rows; r++)
                    for (int c = 0; c < cols; c++)
                        if (board.grid[r][c].state == CellState.COVERED)
                            unknown.add(new int[]{r, c});
                if (unknown.isEmpty()) break;
                int[] pick = unknown.get(rand.nextInt(unknown.size()));
                System.out.println("步骤" + step + ": 概率/随机猜测 (" + pick[0] + "," + pick[1] + ")");
                board.reveal(pick[0], pick[1]);
            }

            System.out.println(board);
            step++;
            if (step > 100) break; // 防止意外死循环
        }

        System.out.println("=== 游戏结束 ===");
        if (board.win) System.out.println("AI获胜！");
        else System.out.println("AI踩到地雷，游戏失败。");
    }
}

七、算法优化方向

本文实现的DPLL是最基础的版本，实际竞赛级SAT求解器还会引入以下增强：

其中CDCL是现代SAT求解器（如MiniSat、Glucose）的核心，它通过在冲突点分析原因并添加学习子句（learned clause），将DPLL从单纯的回溯升级为非时序回溯（backjumping），跳过大量无关分支。

八、复杂度分析

• 时间复杂度：DPLL在最坏情况下为O(2^n)，其中n为变量数。但对于具有大量单位子句和纯文字的实际扫雷约束，平均性能远好于最坏情况。带CDCL的现代求解器可以处理数十万变量的问题。
• 空间复杂度：CNF子句数在最坏情况下为O(C(n, n/2))，其中n为单个数字格邻居数（最大8）。实际上通过at-most/at-least的紧凑编码，可将子句数控制在O(n^2)级别。
• 精确概率计算：枚举所有满足赋值的时间与满足模型数成正比，适用于边界变量少于25个的情况。更大规模需要使用近似采样（如MCMC）或模型计数器（如 sharpSAT）。

九、总结

扫雷看似是一个简单的点击游戏，其底层却隐藏着深刻的计算复杂性。本文展示了如何将扫雷的局部约束转化为全局的布尔可满足性问题，并用经典的DPLL算法进行求解。读者通过本文可以掌握：命题逻辑建模、CNF转化、单位传播、纯文字消除和回溯搜索等SAT求解核心技术。这套方法不仅适用于扫雷，同样适用于数独、逻辑谜题、电路验证、软件测试用例生成等任何可编码为布尔约束的场景，是人工智能和形式化方法领域的基石算法之一。