マインスイーパー ― 数字のヒントから安全なマスを推理する

マインスイーパー ― 数字のヒントから安全なマスを推理する#

この章で学ぶこと#

マインスイーパーは、開いたマスの数字を手がかりに、地雷の場所を推理するパズルです。この章では、その推理を Z3 に任せます。

  • 未開封のマスを Bool 変数で表す

  • 「周囲の数字＝周囲の地雷の数」を制約にする

  • 背理法で「絶対に安全なマス」と「絶対に地雷のマス」を決める（push() / check() / pop()）

人間が指で開けていく作業を、Z3 が代わりにやってくれるわけです。

マインスイーパーのルール#

盤面の数字は、そのマスの周囲8マスにある地雷の数を表します。数字のマスは開いていて安全、. はまだ開けていないマスです。

この章で作るプログラムは、与えられた盤面から地雷でないと断定できるマスを探します。

解き方の考え方#

マス1つ1つについて、次の2通りの仮定を試します。

  1. 「このマスに地雷がある」と仮定して、制約と矛盾するか調べる

    • 矛盾する（unsat）→ 地雷はありえない → 安全なマス

  2. 「このマスに地雷はない」と仮定して、制約と矛盾するか調べる

    • 矛盾する（unsat）→ 地雷が確定 → 地雷のマス

  3. どちらも矛盾しない → まだ決められない（運が悪ければ開けると爆発する）

これを「背理法」と呼びます。仮定を足して矛盾が出れば、仮定が間違っていたと分かる、という考え方です。

一時的に足した仮定は、solver.push()（状態を保存）と solver.pop()（保存した状態に戻す）ではさんで、次のマスの判定に持ち越さないようにします。

コード#

3つの関数を作ります。

  • 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 が安全です。

数字マスの周囲にある未開封マスだけを作ります。数字と接していないマスは、ヒントが何もないので判定のしようがないからです。

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() ではさんで、次の判定に持ち越さない

  • どちらも矛盾しないマスは決められない。マインスイーパーで「運が悪いと爆発する」のはこのため