So we're given a 16x16 minesweepr map, and need to beat it in under a minute. Time to use z3!
Z3 is a Symmetric Modulo Theory (SMT) solver. Essentially, it is 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
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):
# 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, emptiesHere we also state that if you are a number, than you're automatically not 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 to ensure that it was done.
The counts later get transformed into z3 constraints
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 == countWe then need to find a safe square to choose. We pick one of the perimeter squares that is adjacent, and we test it. If we mark it as 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 it as such. We track the known flags in a separate array FLAGGED.
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)Then we just loop until victory.
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!")
breakThe first time I did this, I forgot the BASE_CONSTRAINTS. Surprisingly, the solver was still able to work out safe moves. However, it was much slower. Putting the BASE_CONSTRAINTS in resulted in much faster solve times.
from pwn import *
import re
import 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()