[original](https://gist.github.com/cwgreene/e4ca5404db149eb76afe0b3d804c738c)# Defenit 2020: minesweeper
So we're given a 16x16 minesweepr map, and need to beat it inunder a minute. Time to use z3!
Z3 is a Symmetric Modulo Theory (SMT) solver. Essentially, itis able to solve logic puzzles. Our approach is to parse the map,and for each number encode that as a constraint.
Parsing the map, we first
```pythondef parse_map(grid, bombmap):    rows = bombmap.split("\n")    rows = rows[2::2]    counts = []    empties = []    for i, row in enumerate(rows[:-1]):        row = row[row.index('|'):]        rowcounts = row.split('|')[1:-1]        for j, count in enumerate(rowcounts):            if re.match(" *[0-9]+ *", count):                # Numbers are not mines, direct z3 constraint                BASE_CONSTRAINTS.append(grid[(i,j)]==0)                # Constraints                counts.append((i, j, int(count)))            elif count == "   ":                empties.append((i,j))    return counts, empties```
Here we also state that if you are a number, than you're automaticallynot a mine (encoded as '0'). Setting the BASE_CONSTRAINTS here is a bit of a hack. It would have been better to do it in the construct_constraints,but I had forgotten to do it the first time round and I just wanted toensure that it was done.
The `counts` later get transformed into z3 constraints
```pythondef construct_constraint(grid, i, j, count):    neighbor_sum = 0    for neighbor in neighbors(i,j):        ix, jx = neighbor        neighbor_sum += grid[(ix,jx)]    return neighbor_sum == count```
We then need to find a safe square to choose. We pick one of theperimeter squares that is adjacent, and we test it. If we mark itas a mine, and it can't be, z3 will tell us this isn't satisfiable.This becomes one of our choices. Likewise, if it *must* be mine, we mark itas such. We track the known flags in a separate array FLAGGED.
```pythondef make_choice(grid, counts, empties):    constraints = BASE_CONSTRAINTS[:]    counted = set()    for (i,j,count) in counts:        counted.add((i,j))        constraints.append(construct_constraint(grid, i, j, count))
    choices = []    safe = []    for e in empties:        if not set(neighbors(*e)).intersection(counted):            continue        s = z3.Solver()        s.add(*constraints)        s.add(*FLAGGED)        s.add(*safe)        s.add(grid[e] == 1)        check = s.check()        if check == z3.unsat:            choices.append(e)            safe.append(grid[e]==0)
    flaggable = []    for e in empties:        if not set(neighbors(*e)).intersection(counted):            continue                                                                                                                                             s = z3.Solver()        s.add(*constraints)        s.add(*FLAGGED)        s.add(grid[e] == 0)        check = s.check()        if check == z3.unsat:            flaggable.append(e)            FLAGGED.append(grid[e] == 1)    return choices, set(flaggable)```
Then we just loop until victory.```python    while True:        print("Parsing...")        counts, empties = parse_map(grid, bombmap)        if not empties:            break        print("Thinking...")        choices, flaggable = make_choice(grid, counts, empties)        print("Thought!")        for bomb in flaggable:            print(convert(*bomb)+"f")            r.sendline(convert(*bomb)+"f")            bombmap = recv_map()            print(bombmap)        for choice in choices:            print(convert(*choice))            r.sendline(convert(*choice))            bombmap = recv_map()            print(bombmap)        if not choices:            print("Done!")            break```
The first time I did this, I forgot the BASE_CONSTRAINTS. Surprisingly,the solver was still able to work out safe moves. However, it was muchslower. Putting the BASE_CONSTRAINTS in resulted in much faster solve times.
## Appendix A: Full code
```pythonfrom pwn import *
import reimport z3
r = remote("minesweeper.ctf.defenit.kr", 3333)
BASE_CONSTRAINTS = []FLAGGED = []
def init_grid():    grid = {}    for i in range(16):        for j in range(16):            grid[(i,j)] = z3.Int("({},{})".format(i,j))            BASE_CONSTRAINTS.append(grid[(i,j)] >= 0)            BASE_CONSTRAINTS.append(grid[(i,j)] <= 1)    return grid
def recv_map():    print(r.recvuntil('     a'))    bombmap = b"     a"+ r.recvuntil('-\n\n')    if b'X' in bombmap:        print(str(bombmap, 'ascii'))        print(str(r.recv(), 'ascii'))    return str(bombmap, 'ascii')
def parse_map(grid, bombmap):    rows = bombmap.split("\n")    rows = rows[2::2]    counts = []    empties = []    for i, row in enumerate(rows[:-1]):        row = row[row.index('|'):]        rowcounts = row.split('|')[1:-1]        for j, count in enumerate(rowcounts):            if re.match(" *[0-9]+ *", count):                BASE_CONSTRAINTS.append(grid[(i,j)]==0)                counts.append((i, j, int(count)))            elif count == "   ":                empties.append((i,j))    return counts, empties
def convert(row, column):    c = "abcdefghijklmnopqrst"[column]    r = [str(i) for i in range(1,17)][row]    return c+r
def neighbors(i,j):    result = []    for x in [1,0,-1]:        for y in [1,0,-1]:            if x == 0 and y == 0:                continue            if (i + x >= 16) or (i + x < 0) or (j + y >= 16) or (j + y < 0):                continue            result.append((i+x, j+y))    return result
def construct_constraint(grid, i, j, count):    neighbor_sum = 0    for neighbor in neighbors(i,j):        ix, jx = neighbor        neighbor_sum += grid[(ix,jx)]    return neighbor_sum == count
def make_choice(grid, counts, empties):    constraints = BASE_CONSTRAINTS[:]    counted = set()    for (i,j,count) in counts:          counted.add((i,j))        constraints.append(construct_constraint(grid, i, j, count))
    choices = []    safe = []    for e in empties:        if not set(neighbors(*e)).intersection(counted):            continue        s = z3.Solver()        s.add(*constraints)        s.add(*FLAGGED)        s.add(*safe)        s.add(grid[e] == 1)        check = s.check()        if check == z3.unsat:            choices.append(e)            safe.append(grid[e]==0)
    flaggable = []    for e in empties:        if not set(neighbors(*e)).intersection(counted):            continue        s = z3.Solver()        s.add(*constraints)        s.add(*FLAGGED)        s.add(grid[e] == 0)        check = s.check()        if check == z3.unsat:            flaggable.append(e)            FLAGGED.append(grid[e] == 1)    return choices, set(flaggable)
def main():    grid = init_grid()
    bombmap = recv_map()    # choose 3 random spots to kick off.    r.sendline("a5")    bombmap = recv_map()    r.sendline("n5")    bombmap = recv_map()    r.sendline("j12")    bombmap = recv_map()    print(bombmap)    # main loop    flagged = set()    while True:        print("Parsing...")        counts, empties = parse_map(grid, bombmap)        if not empties:            break        print("Thinking...")        choices, flaggable = make_choice(grid, counts, empties)        print("Thought!")        for bomb in flaggable:            print(convert(*bomb)+"f")            r.sendline(convert(*bomb)+"f")            bombmap = recv_map()            print(bombmap)        for choice in choices:            print(convert(*choice))            r.sendline(convert(*choice))            bombmap = recv_map()            print(bombmap)        if not choices:            print("Done!")            break            #for empty in (set(empties) - flaggable):            #    r.sendline(convert(*empty)+"f")            #break    r.interactive()
main()```
# References1. https://yurichev.com/blog/minesweeper/