每日算法 — 使用java实现扫雷：SAT求解器归约与DPLL单元传播判定

引言

扫雷（Minesweeper）不仅是一款经典益智游戏，还被证明是NP完全问题。本文使用Java将扫雷局面归约为布尔可满足性问题（SAT），并应用经典的DPLL算法配合单元传播（Unit Propagation）启发式，让AI能够精确判定哪些格子必然安全、哪些格子必然有雷，以及哪些格子需要概率推断。

算法核心思想

从扫雷到SAT的归约

扫雷的约束条件天然适合用布尔变量表达：
– 对每个未揭示的邻居格子 $x_i$，定义布尔变量：$x_i = true$ 表示有雷
– 每个已揭示的数字格 $n$ 产生一个约束：其周围未揭示格子中恰好有 $n$ 个雷

例如，数字”2″周围有3个未揭示格子 $a,b,c$，则约束为：
$$a + b + c = 2$$

这可以分解为CNF（合取范式）：
– $(a \lor b)$, $(a \lor c)$, $(b \lor c)$ （至少2个为真）
– $(\neg a \lor \neg b \lor \neg c)$ 且所有两两组合 （至多2个为真）

DPLL算法

DPLL是现代SAT求解器的核心框架：

1. 单元传播：若子句只剩一个未赋值文字，则强制赋值使该子句满足
2. 纯文字消除：若某变量在所有子句中只以正/负形式出现，直接赋值
3. 分支选择：选一个变量尝试true/false，递归求解
4. 冲突学习：遇到矛盾时回溯，并学习新子句避免重复犯错

Java实现

核心数据结构

import java.util.*;

public class MinesweeperSAT {
    static final int ROWS = 16;
    static final int COLS = 30;
    static final int MINES = 99;

    // 游戏状态
    int[][] board = new int[ROWS][COLS]; // -1=雷, 0-8=数字
    boolean[][] revealed = new boolean[ROWS][COLS];
    boolean[][] flagged = new boolean[ROWS][COLS];
    boolean gameOver = false;
    Random rand = new Random();

    // SAT表示：变量ID = r * COLS + c
    // 正文字表示有雷，负文字表示无雷
    List<Set<Integer>> clauses = new ArrayList<>();
    Map<Integer, Boolean> assignment = new HashMap<>();

    void initBoard() {
        // 随机布雷
        int minesPlaced = 0;
        while (minesPlaced < MINES) {
            int r = rand.nextInt(ROWS);
            int c = rand.nextInt(COLS);
            if (board[r][c] != -1) {
                board[r][c] = -1;
                minesPlaced++;
            }
        }
        // 计算数字
        for (int r = 0; r < ROWS; r++) {
            for (int c = 0; c < COLS; c++) {
                if (board[r][c] == -1) continue;
                int count = 0;
                for (int dr = -1; dr <= 1; dr++) {
                    for (int dc = -1; dc <= 1; dc++) {
                        int nr = r + dr, nc = c + dc;
                        if (inBounds(nr, nc) && board[nr][nc] == -1) count++;
                    }
                }
                board[r][c] = count;
            }
        }
    }

    boolean inBounds(int r, int c) {
        return r >= 0 && r < ROWS && c >= 0 && c < COLS;
    }

    int varId(int r, int c) {
        return r * COLS + c + 1; // 变量从1开始
    }

约束生成：从数字格到CNF

    /**
     * 为指定数字格生成CNF约束
     * 约束：neighbors中恰好有mineCount个变量为true
     */
    void generateConstraint(int r, int c) {
        if (!revealed[r][c] || board[r][c] <= 0) return;

        List<Integer> neighbors = new ArrayList<>();
        for (int dr = -1; dr <= 1; dr++) {
            for (int dc = -1; dc <= 1; dc++) {
                int nr = r + dr, nc = c + dc;
                if ((dr != 0 || dc != 0) && inBounds(nr, nc) 
                    && !revealed[nr][nc] && !flagged[nr][nc]) {
                    neighbors.add(varId(nr, nc));
                }
            }
        }

        int mineCount = board[r][c];
        // 减去已标记的雷数
        for (int dr = -1; dr <= 1; dr++) {
            for (int dc = -1; dc <= 1; dc++) {
                int nr = r + dr, nc = c + dc;
                if ((dr != 0 || dc != 0) && inBounds(nr, nc) && flagged[nr][nc]) {
                    mineCount--;
                }
            }
        }

        if (mineCount < 0 || mineCount > neighbors.size()) return;
        if (neighbors.isEmpty()) return;

        // 生成"至少mineCount个为真"的子句
        generateAtLeast(neighbors, mineCount);
        // 生成"至多mineCount个为真"的子句
        generateAtMost(neighbors, mineCount);
    }

    /**
     * 生成"列表中至少k个为真"的CNF子句
     * 方法：所有大小为(n-k+1)的组合取反
     */
    void generateAtLeast(List<Integer> vars, int k) {
        int n = vars.size();
        if (k <= 0) return;
        if (k > n) { clauses.add(new HashSet<>(Arrays.asList(1, -1))); return; } // 矛盾

        // 使用组合生成：C(n, n-k+1) 个子句
        List<int[]> combinations = generateCombinations(n, n - k + 1);
        for (int[] comb : combinations) {
            Set<Integer> clause = new HashSet<>();
            for (int idx : comb) {
                clause.add(vars.get(idx)); // 正文字
            }
            clauses.add(clause);
        }
    }

    /**
     * 生成"列表中至多k个为真"的CNF子句
     * 方法：所有大小为(k+1)的组合全取反
     */
    void generateAtMost(List<Integer> vars, int k) {
        int n = vars.size();
        if (k >= n) return;
        if (k < 0) { clauses.add(new HashSet<>(Arrays.asList(1, -1))); return; }

        List<int[]> combinations = generateCombinations(n, k + 1);
        for (int[] comb : combinations) {
            Set<Integer> clause = new HashSet<>();
            for (int idx : comb) {
                clause.add(-vars.get(idx)); // 负文字
            }
            clauses.add(clause);
        }
    }

    /**
     * 生成从n个元素中选k个的所有组合索引
     */
    List<int[]> generateCombinations(int n, int k) {
        List<int[]> result = new ArrayList<>();
        int[] comb = new int[k];
        for (int i = 0; i < k; i++) comb[i] = i;

        while (true) {
            result.add(comb.clone());
            int i = k - 1;
            while (i >= 0 && comb[i] == n - k + i) i--;
            if (i < 0) break;
            comb[i]++;
            for (int j = i + 1; j < k; j++) comb[j] = comb[j-1] + 1;
        }
        return result;
    }

DPLL求解器核心

    /**
     * DPLL主函数：返回所有可推导的赋值
     */
    Map<Integer, Boolean> solveDPLL(List<Set<Integer>> cls, Map<Integer, Boolean> assign) {
        // 复制避免修改原数据
        List<Set<Integer>> clauses = new ArrayList<>();
        for (Set<Integer> cl : cls) clauses.add(new HashSet<>(cl));
        Map<Integer, Boolean> assignment = new HashMap<>(assign);

        // 单元传播循环
        while (true) {
            boolean changed = false;
            Iterator<Set<Integer>> it = clauses.iterator();
            while (it.hasNext()) {
                Set<Integer> clause = it.next();
                // 简化子句
                Set<Integer> simplified = simplifyClause(clause, assignment);
                if (simplified == null) { // 已满足
                    it.remove();
                    continue;
                }
                if (simplified.isEmpty()) { // 矛盾
                    return null;
                }
                if (simplified.size() == 1) { // 单元子句
                    int lit = simplified.iterator().next();
                    int var = Math.abs(lit);
                    boolean val = lit > 0;
                    if (assignment.containsKey(var) && assignment.get(var) != val) {
                        return null; // 冲突
                    }
                    if (!assignment.containsKey(var)) {
                        assignment.put(var, val);
                        changed = true;
                    }
                    it.remove();
                }
            }
            if (!changed) break;
        }

        if (clauses.isEmpty()) return assignment; // 全部满足

        // 选择分支变量（未赋值变量中出现频率最高的）
        int branchVar = selectBranchVariable(clauses, assignment);
        if (branchVar == 0) return assignment;

        // 尝试true
        Map<Integer, Boolean> assignCopy = new HashMap<>(assignment);
        assignCopy.put(branchVar, true);
        Map<Integer, Boolean> result = solveDPLL(clauses, assignCopy);
        if (result != null) return result;

        // 尝试false
        assignCopy = new HashMap<>(assignment);
        assignCopy.put(branchVar, false);
        return solveDPLL(clauses, assignCopy);
    }

    /**
     * 用当前赋值简化子句
     */
    Set<Integer> simplifyClause(Set<Integer> clause, Map<Integer, Boolean> assignment) {
        Set<Integer> result = new HashSet<>();
        for (int lit : clause) {
            int var = Math.abs(lit);
            if (!assignment.containsKey(var)) {
                result.add(lit);
            } else if ((lit > 0) == assignment.get(var)) {
                return null; // 子句已满足
            }
            // 否则该文字为假，跳过
        }
        return result;
    }

    /**
     * 选择分支变量：使用MOMS启发式（最小出现次数中尺寸最小）
     */
    int selectBranchVariable(List<Set<Integer>> clauses, Map<Integer, Boolean> assignment) {
        Map<Integer, Integer> freq = new HashMap<>();
        for (Set<Integer> cl : clauses) {
            for (int lit : cl) {
                int var = Math.abs(lit);
                if (!assignment.containsKey(var)) {
                    freq.put(var, freq.getOrDefault(var, 0) + 1);
                }
            }
        }
        int bestVar = 0, bestFreq = 0;
        for (Map.Entry<Integer, Integer> e : freq.entrySet()) {
            if (e.getValue() > bestFreq) {
                bestFreq = e.getValue();
                bestVar = e.getKey();
            }
        }
        return bestVar;
    }

扫雷AI决策逻辑

    /**
     * AI决策：使用SAT求解找到所有必然安全的格子和必然有雷的格子
     */
    void aiMove() {
        if (gameOver) return;

        // 1. 收集所有边界约束（已揭示数字格与未揭示格相邻）
        clauses.clear();
        assignment.clear();

        for (int r = 0; r < ROWS; r++) {
            for (int c = 0; c < COLS; c++) {
                if (revealed[r][c] && board[r][c] > 0) {
                    generateConstraint(r, c);
                }
            }
        }

        if (clauses.isEmpty()) {
            // 开局或边界无约束，随机点击
            randomReveal();
            return;
        }

        // 2. 对边界每个未揭示变量，测试是否为雷/安全
        Set<Integer> borderVars = new HashSet<>();
        for (Set<Integer> cl : clauses) borderVars.addAll(cl);

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

        for (int var : borderVars) {
            if (Math.abs(var) > ROWS * COLS) continue;
            int vid = Math.abs(var);

            // 测试 var = true（有雷）
            Map<Integer, Boolean> test1 = new HashMap<>();
            test1.put(vid, true);
            boolean canBeMine = solveDPLL(clauses, test1) != null;

            // 测试 var = false（安全）
            Map<Integer, Boolean> test2 = new HashMap<>();
            test2.put(vid, false);
            boolean canBeSafe = solveDPLL(clauses, test2) != null;

            int cellR = (vid - 1) / COLS;
            int cellC = (vid - 1) % COLS;

            if (!canBeMine && canBeSafe) {
                safeCells.add(new int[]{cellR, cellC});
            } else if (canBeMine && !canBeSafe) {
                mineCells.add(new int[]{cellR, cellC});
            }
        }

        // 3. 优先标记确定的雷，然后揭示确定的安全格
        for (int[] cell : mineCells) {
            if (!flagged[cell[0]][cell[1]]) {
                flagged[cell[0]][cell[1]] = true;
                System.out.printf("标记雷: (%d, %d)%n", cell[0], cell[1]);
            }
        }

        for (int[] cell : safeCells) {
            if (!revealed[cell[0]][cell[1]]) {
                reveal(cell[0], cell[1]);
                System.out.printf("揭示安全格: (%d, %d)%n", cell[0], cell[1]);
            }
        }

        // 4. 若没有确定格，使用概率推断或随机
        if (safeCells.isEmpty() && mineCells.isEmpty()) {
            probabilityGuess();
        }
    }

    void reveal(int r, int c) {
        if (!inBounds(r, c) || revealed[r][c] || flagged[r][c]) return;
        revealed[r][c] = true;
        if (board[r][c] == -1) {
            gameOver = true;
            System.out.println("踩到雷! 游戏结束!");
        } else if (board[r][c] == 0) {
            // 自动揭示周围
            for (int dr = -1; dr <= 1; dr++) {
                for (int dc = -1; dc <= 1; dc++) {
                    reveal(r + dr, c + dc);
                }
            }
        }
    }

    void randomReveal() {
        List<int[]> candidates = new ArrayList<>();
        for (int r = 0; r < ROWS; r++) {
            for (int c = 0; c < COLS; c++) {
                if (!revealed[r][c] && !flagged[r][c]) {
                    candidates.add(new int[]{r, c});
                }
            }
        }
        if (!candidates.isEmpty()) {
            int[] cell = candidates.get(rand.nextInt(candidates.size()));
            reveal(cell[0], cell[1]);
            System.out.printf("随机揭示: (%d, %d)%n", cell[0], cell[1]);
        }
    }

    void probabilityGuess() {
        // 简化的概率猜测：选择约束中概率最低的格子
        System.out.println("无确定解，进行概率猜测...");
        randomReveal();
    }

运行演示

    void printBoard() {
        for (int r = 0; r < ROWS; r++) {
            for (int c = 0; c < COLS; c++) {
                if (flagged[r][c]) System.out.print("F ");
                else if (!revealed[r][c]) System.out.print("# ");
                else if (board[r][c] == -1) System.out.print("* ");
                else if (board[r][c] == 0) System.out.print(". ");
                else System.out.print(board[r][c] + " ");
            }
            System.out.println();
        }
    }

    void play() {
        initBoard();
        // 第一步安全点击中心区域
        reveal(ROWS/2, COLS/2);

        int moves = 0;
        while (!gameOver && moves < 200) {
            aiMove();
            moves++;
        }

        System.out.println("\n最终局面:");
        printBoard();
        if (!gameOver) {
            int unrevealed = 0;
            for (int r = 0; r < ROWS; r++)
                for (int c = 0; c < COLS; c++)
                    if (!revealed[r][c]) unrevealed++;
            System.out.println("未揭示格子: " + unrevealed + ", 步数: " + moves);
        }
    }

    public static void main(String[] args) {
        MinesweeperSAT game = new MinesweeperSAT();
        game.play();
    }

复杂度分析

总结

本文将扫雷AI建立在严格的SAT求解框架之上，通过CNF归约将每个数字格的局部约束编码为布尔公式，再利用DPLL+单元传播推导全局必然结论。相比纯概率推理，SAT方法能保证在逻辑上必然正确的判定。读者可在此基础上引入冲突驱动子句学习（CDCL）、 watched literals等现代SAT优化技术，将AI的求解效率提升数个数量级。