扫雷：根据已翻开格中的数字推断出哪些格是安全的

扫雷：根据已翻开格中的数字推断出哪些格是安全的#

本章的内容#

扫雷是借助已翻开格中的数字推断地雷位置的游戏，本章把这一推断交给 Z3 去做。

  • 用 Bool 变量表示尚未翻开的格

  • 把周围的数字等于周围地雷的数目写成约束

  • 用反证法判定绝对安全的格与绝对是地雷的格，即 push()、check()、pop()

人工逐格翻开的工作，由 Z3 代为完成。本章的重点不在扫雷本身，而在反证法：同一套写法可以搬到任何“假设与约束相矛盾”的判断上。

扫雷的规则#

盘面上的数字表示该格周围 8 格中地雷的数目，带数字的格已经翻开，因而是安全的格，. 则表示尚未翻开的格，需要由程序推断。每一格只有有雷与无雷两种状态，数字给出的是相邻格中状态的数目，这两点合起来就是一组约束。

本章要写的程序，就是从给定的盘面中找出那些可以断定不是地雷的格，把它们标记出来，再显示成盘面的形状。

解题的思路#

对每一格分别试下面两种假设。

  1. 假设这一格有地雷，检查是否与约束矛盾

    • 若结果为矛盾，即 unsat，则不可能有地雷，该格是安全的

  2. 假设这一格没有地雷，检查是否与约束矛盾

    • 若结果为矛盾，即 unsat，则地雷确定，该格是地雷

  3. 两种假设都不矛盾，则尚不能判定，翻开时可能踩中地雷

这种做法称为反证法，即追加假设之后导出矛盾，便可知道假设是错的。反证法之所以够用，是因为约束已经涵盖全部可行解。若“这一格有雷”与约束矛盾，那么每一个可行解里这一格都没有雷，判定不依赖运气。

临时追加的假设，要用 solver.push() 与 solver.pop() 夹住，判定完之后回到原来的状态，以免把它带到下一格的判定中去。

代码#

程序中要写三个函数。

  • get_neighbors()：返回某一格周围的 8 格

  • solve_board()：求解盘面，返回安全的格与地雷的格，内部完成建立变量、追加约束与逐格判定三件事

  • show_result()：把结果显示成盘面的形状

三个函数按流程分工：先取邻格，再建立约束，最后把判定结果画出来。

from z3 import *

# 8 个方向（上下左右＋斜向）
DIRECTIONS = [
    (-1, -1), (-1, 0), (-1, 1),
    (0, -1),           (0, 1),
    (1, -1),  (1, 0),  (1, 1),
]


def get_neighbors(x, y, h, w):
    """返回格子 (x, y) 周围 8 格中位于盘面内的那些"""
    neighbors = []
    for dx, dy in DIRECTIONS:
        nx, ny = x + dx, y + dy
        if 0 <= nx < w and 0 <= ny < h:
            neighbors.append((nx, ny))
    return neighbors


def solve_board(board_text):
    """求解盘面，返回 (安全格, 地雷格)"""
    rows = board_text.strip().split()
    h, w = len(rows), len(rows[0])

    # 给数字格周围的未翻开格子建一个表示“有地雷”的 Bool 变量
    mine = {}
    for y, row in enumerate(rows):
        for x, v in enumerate(row):
            if v == '.':
                continue                      # 未翻开的格子本身跳过
            for nx, ny in get_neighbors(x, y, h, w):
                if rows[ny][nx] == '.':
                    mine[nx, ny] = Bool(f'mine_{nx}_{ny}')

    # 约束条件：数字格周围为 True 的变量个数 = 这个数字
    solver = Solver()
    for y, row in enumerate(rows):
        for x, v in enumerate(row):
            if v == '.':
                continue
            around = [mine[loc] for loc in get_neighbors(x, y, h, w) if loc in mine]
            if around:
                solver.add(Sum(around) == int(v))

    # 给每个格子加上假设，看是否矛盾
    safe, mines = [], []
    for (x, y), var in mine.items():
        solver.push()
        solver.add(var)                   # 假设：这里有地雷
        if solver.check() == unsat:       # 矛盾 → 不是地雷
            safe.append((x, y))
        solver.pop()

        solver.push()
        solver.add(Not(var))              # 假设：这里没有地雷
        if solver.check() == unsat:       # 矛盾 → 确定是地雷
            mines.append((x, y))
        solver.pop()

    return safe, mines


def show_result(board_text, safe, mines):
    """“#”是安全格，“*”是地雷格"""
    board = [list(row) for row in board_text.strip().split()]
    for x, y in mines:
        board[y][x] = '*'
    for x, y in safe:
        board[y][x] = '#'
    print("\n".join(" ".join(row) for row in board))

运行示例#

minesweeper

下面求解这个盘面。

board_str = """
...201..................
...201..................
...1013.................
...1102.................
....1011123.............
..21100012...22211122...
..2000012.33212.3111....
..421002.310002.3.122...
....3224.31000112111....
........4.20000001121...
.......43.20000012.11...
.......3122211001.212...
.......202.3.10011213...
......2103.42210001.213.
......1112.43.111233202.
......2.222..311.3..212.
.............2124.4.....
............111.3.......
........................
........................
"""

safe, mines = solve_board(board_str)
print(f"安全格: {len(safe)} 个")
print(f"地雷格: {len(mines)} 个")
show_result(board_str, safe, mines)

安全格: 43 个
地雷格: 54 个
. . * 2 0 1 # . . . . . . . . . . . . . . . . .
. . * 2 0 1 * # . . . . . . . . . . . . . . . .
. . # 1 0 1 3 * . . . . . . . . . . . . . . . .
. . # 1 1 0 2 * # # * # . . . . . . . . . . . .
. # # * 1 0 1 1 1 2 3 # # # * # # # * # # . . .
. . 2 1 1 0 0 0 1 2 * * * 2 2 2 1 1 1 2 2 . . .
. . 2 0 0 0 0 1 2 * 3 3 2 1 2 * 3 1 1 1 * # . .
. * 4 2 1 0 0 2 * 3 1 0 0 0 2 * 3 * 1 2 2 # . .
. . * * 3 2 2 4 * 3 1 0 0 0 1 1 2 1 1 1 * # . .
. . . * * # * * 4 * 2 0 0 0 0 0 0 1 1 2 1 # . .
. . . . . . * 4 3 * 2 0 0 0 0 0 1 2 * 1 1 # . .
. . . . . . * 3 1 2 2 2 1 1 0 0 1 * 2 1 2 * . .
. . . . . * * 2 0 2 * 3 * 1 0 0 1 1 2 1 3 * # .
. . . . . # 2 1 0 3 * 4 2 2 1 0 0 0 1 * 2 1 3 .
. . . . . # 1 1 1 2 * 4 3 * 1 1 1 2 3 3 2 0 2 .
. . . . . # 2 * 2 2 2 * * 3 1 1 * 3 * * 2 1 2 .
. . . . . . . # * # # # * 2 1 2 4 * 4 # . . # .
. . . . . . . . . . . # 1 1 1 * 3 * # # . . . .
. . . . . . . . . . . # # # # # # # . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .

未翻开的格共有 111 个，其中 43 个确定为安全，54 个确定为地雷，其余 14 个无论假设哪一种都不矛盾，因此无法判定。人玩这局游戏时，这 14 个格到最后也无法判定，只能凭运气翻开，一旦踩中地雷就结束。

盘面中的 # 表示安全的格，* 表示地雷的格。

代码的说明#

1. 建立变量#

mine = {}
for y, row in enumerate(rows):
    for x, v in enumerate(row):
        if v == '.':
            continue
        for nx, ny in get_neighbors(x, y, h, w):
            if rows[ny][nx] == '.':
                mine[ny, nx] = Bool(f'mine_{ny}_{nx}')

mine 是 (x, y) → Bool 变量 的字典，变量的含义是该格是否有地雷，True 表示有地雷，False 表示安全。

只对数字格周围那些尚未翻开的格建立变量。与数字不相邻的格没有任何提示，无从判定，因此不会出现在 mine 里，判定时也不会被访问。

2. 追加约束#

around = [mine[loc] for loc in get_neighbors(x, y, h, w) if loc in mine]
if around:
    solver.add(Sum(around) == int(v))

对数字格 v 追加约束，使周围未翻开格中地雷的数目等于 v。

Sum(around) 是 Bool 变量之和，Z3 会把 True 当作 1、False 当作 0 相加，因此这个和就是周围地雷的数目。

around 为空的情形，是数字格的周围全部已经翻开的时候。此时没有可加的约束，用 if around: 跳过。

3. 用反证法判定#

solver.push()
solver.add(var)                   # 假设：这里有地雷
if solver.check() == unsat:       # 矛盾 → 不是地雷
    safe.append((x, y))
solver.pop()

调用

作用

solver.push()

保存当前的约束，以便追加临时约束

solver.add(...)

追加假设

solver.check()

在追加假设的状态下检查是否有解，若为 unsat 则矛盾

solver.pop()

回到保存的状态，即丢弃假设

如果忘记 pop()，上一格的假设就会残留到下一格的判定中，结果随之出错，因此 push() 与 pop() 必须成对使用。代价是每一格都要重新求解一次，格数一多，判定时间会随之增长。

小结#

  • 把未翻开的格设为 Bool 变量之后，周围的地雷数就可以写成 Sum(...) == 数字

  • 假设有地雷而得到 unsat，则该格安全；假设没有地雷而得到 unsat，则确定该格有地雷，反证法正是这样做的

  • 临时假设用 push() 与 pop() 夹住，不要带到下一次判定

  • 两种假设都不矛盾的格无法判定，扫雷中运气不好就会爆炸，原因正在于此