5-Mar-2017: Cracking Minesweeper with Z3 SMT solver

(The following text has been moved to the article at https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.)

For those who are not very good at playing Minesweeper (like me), it's possible to predict bombs' placement without touching debugger.

Here is a clicked somewhere and I see revealed empty cells and cells with known number of "neighbours":

What we have here, actually? Hidden cells, empty cells (where bombs are not present), and empty cells with numbers, which shows how many bombs are placed nearby. Here is what we can do: we will try to place a bomb to all possible hidden cells and ask Z3 SMT solver, if it can disprove the very fact that the bomb can be placed there.

The method

Take a look at this fragment. "?" mark is for unknown cell, "." is for empty cell, digit is a number of neighbours.

? ? ?
? 3 .
? 1 .

So there are 5 unknown cells. We will try each unknown cell by placing a bomb there. Let's first pick top/left cell:

1 ? ?
? 3 .
? 1 .

Then we will try to solve the following system of equations (RrCc is cell of row r and column c):

R1C2+R2C1+R2C2=1                               (because we placed bomb at R1C1)
R2C1+R2C2+R3C1=1                               (because we have "1" at R3C2)
R1C1+R1C2+R1C3+R2C1+R2C2+R2C3+R3C1+R3C2+R3C3=3 (because we have "3" at R2C2)
R1C2+R1C3+R2C2+R2C3+R3C2+R3C3=0                (because we have "." at R2C3)
R2C2+R2C3+R3C2+R3C3=0                          (because we have "." at R3C3)

As it turns out, this system of equations is satisfiable, so there could be a bomb at this cell. But this information is not interesting to us, since we want to find cells we can freely click on. And we will try another one...

The code

#!/usr/bin/python

known=[
"01?10001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"????1001?",
"????3101?",
"?????211?",
"?????????"]

from z3 import *
import sys

WIDTH=len(known[0])
HEIGHT=len(known)

print "WIDTH=", WIDTH, "HEIGHT=", HEIGHT

def chk_bomb(row, col):

    s=Solver()

    cells=[[Int('cell_r=%d_c=%d' % (r,c)) for c in range(WIDTH+2)] for r in range(HEIGHT+2)]

    # make border
    for c in range(WIDTH+2):
        s.add(cells[0][c]==0)
        s.add(cells[HEIGHT+1][c]==0)
    for r in range(HEIGHT+2):
        s.add(cells[r][0]==0)
        s.add(cells[r][WIDTH+1]==0)

    for r in range(1,HEIGHT+1):
        for c in range(1,WIDTH+1):

            t=known[r-1][c-1]
            if t in "012345678":
                s.add(cells[r][c]==0)
                # we need empty border so the following expression would be able to work for all possible cases:
                s.add(cells[r-1][c-1] + cells[r-1][c] + cells[r-1][c+1] + cells[r][c-1] + cells[r][c+1] + cells[r+1][c-1] + cells[r+1][c] + cells[r+1][c+1]==int(t))

    # place bomb:
    s.add(cells[row][col]==1)

    result=str(s.check())
    if result=="unsat":
        print "row=%d col=%d, unsat!" % (row, col)

# enumerate all hidden cells:
for r in range(1,HEIGHT+1):
    for c in range(1,WIDTH+1):
        if known[r-1][c-1]=="?":
            chk_bomb(r, c)


The code is almost self-explanatory. We need border for the same reason, why Conway's "Game of Life" implementations also has border (to make calculation function simpler). Whenever we know that the cell is free of bomb, we put zero there. Whenever we know number of neighbours, we add a constraint, again, just like in "Game of Life": number of neighbours must be equal to the number we got from the Minesweeper. Then we place bomb somewhere and check.

Let's run:

row=1 col=3, unsat!
row=6 col=2, unsat!
row=6 col=3, unsat!
row=7 col=4, unsat!
row=7 col=9, unsat!
row=8 col=9, unsat!

These are cells where I can click safely, so I did:

Now we have more information, so we update input:

known=[
"01110001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"?11?1001?",
"???331011",
"?????2110",
"???????10"]

I run it again:

row=7 col=1, unsat!
row=7 col=2, unsat!
row=7 col=3, unsat!
row=8 col=3, unsat!
row=9 col=5, unsat!
row=9 col=6, unsat!

I click on these cells again:

I update it again:

known=[
"01110001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"?11?1001?",
"222331011",
"??2??2110",
"????22?10"]
row=8 col=2, unsat!
row=9 col=4, unsat!

This is last update:

known=[
"01110001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"?11?1001?",
"222331011",
"?22??2110",
"???322?10"]

... last result:

row=9 col=1, unsat!
row=9 col=2, unsat!

Voila!

The source code: https://github.com/dennis714/yurichev.com/blob/master/blog/minesweeper/minesweeper_solver.py.

More Z3 examples are in my blog and here: https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.

Some discussion on HN: https://news.ycombinator.com/item?id=13797375.

Update: next part: https://yurichev.com/blog/minesweeper_SAT/.


→ [list of blog posts, my twitter/facebook]

The page last updated on 29-April-2017