## Challenge Description
Take a break from the other challenges and play a relxing game of MinesweeperI have even solved most of the board for you and marked many of the mines.I am completely sure they are correct so you just need to find the remaining ones.
## Intuition
Looking at the minesweeper map, it's huge, but I noticed that the patterns looklike wires and seem to lead to some structure which intuitively resemble logicgates. Even more, there are multiple mentions in the code of _circuits_. So I searchedon the internet for something related to minesweeper and circuits and found a [paper from 2015](https://web.math.ucsb.edu/~padraic/ucsb_2014_15/ccs_problem_solving_w2015/NP3.pdf) which proves that Minesweeper is np-complete using circuits which look exactly like the ones in the challenge.
An initial idea that results is that we could convert the map to a logic circuit and input it intoa sat-solver like **z3**. Now... that's kinda complicated.
The map being partially solved, consistent and built like a circuit means that giving in _input_ toeach end of the wire (aka putting a bomb or not there), should result in a unique arrangement for theentire map. Intuitively, this means that the whole map can be converted into a logic formula and fed toas sat solver.
## Solution
After some more research, I found a github repo with a minesweeper [sat solver](https://github.com/FabianGalis/minesweeper-sat) which structured the map in a very similar way with the one in the given challenge. I modified the code such that it fit the problem:
```pythonfrom pysat.solvers import Solver #for SAT solvingfrom itertools import combinations #for combinations in a CNF
import itertoolsimport hashlib
# DIMACS codificationdef M(i,j,board_w): return  board_w**1 * i + board_w**0 * j + 1
# find unknown cells next to a cell at i,jdef unknown_neighbours(board,i,j):  neighbours=[]  for h in range(i-1,i+2):    for w in range(j-1,j+2):      if h<len(board) and w<len(board[0]) and h>=0 and w>=0 and (board[h][w]>8): neighbours.append((h,w))  return neighbours
# clauses per celldef cell_clauses(board,i,j):  neighbours=unknown_neighbours(board,i,j)  cell_clauses=[]
  #at least n mines  for combination in combinations([M(elem[0],elem[1],len(board[0])) for elem in neighbours],len(neighbours)-board[i][j]+1):    cell_clauses.append(list(combination))
  #at most n mines  for combination in combinations([-M(elem[0],elem[1],len(board[0])) for elem in neighbours], board[i][j]+1):    cell_clauses.append(list(combination))
  return cell_clauses
# clauses per boarddef board_clauses(board,board_h,board_w):  clauses=[]  for i in range(board_h):    for j in range(board_w):       if board[i][j]<9:        #add self as known safe cell        clauses.append([-M(i,j,board_w)])        #add surrounding constraints        clauses+=cell_clauses(board,i,j)      elif board[i][j]==10:        #add self as mine cell        clauses.append([M(i,j,board_w)])  return clauses
#print solutiondef show_solution(board,board_h,board_w,model):  bits = []  for i in range(board_h):    for j in range(board_w):      if board[i][j]==9:          board[i][j]='m' if M(i, j,board_w) in model else 's'      if i == 23:          bit = 1 if board[i][j] == 'm' else 0          bits.append(bit)      flag = hashlib.sha256(bytes(bits)).hexdigest()      print(f'Flag: CTF{{{flag}}}') 
def solve_board(board,printing=True):  if printing:    print("Legend:\n0-8: mines nearby\n9  : unknown\n10 : known mine")
  board_w=len(board[0])  board_h=len(board)
  s = Solver(name='cd')  s.append_formula(board_clauses(board,board_h,board_w))
  if s.solve():    model=s.get_model()    show_solution(board,board_h,board_w,model)    if printing:      print("\nSAT - consistent")      print("Model:",model)      print("Legend:\n0-8: mines nearby\n9  : unknown\n10 : known mine\nm  : found mine\ns  : found safe")
    return True  else:    print("\nUNSAT - inconsistent")    return False
#board encoding:#0-8: mines nearby#9  : unknown space#10 : known mine
with open('gameboard.txt', 'r') as fin:    circuit = fin.read()    circuit = circuit.replace(' ', '0')    circuit = [list(line) for line in circuit.split('\n') if len(line) > 0]
board_width = len(circuit[0])board_height = len(circuit)mine_count=0 #smaller than width*heightunknown_cells=0 #smaller than width*height
board = [[None for x in range(board_width)] for y in range(board_height)]
for i, (x, y) in enumerate(itertools.product(range(board_width), range(board_height))):    val = int(circuit[y][x], 16)    if val == 11:        val = 10    if val == 10:        mine_count += 1    elif val == 9:        unknown_cells += 1
    board[y][x] = val
solve_board(board)```
Running this for 1 minute gets the flag.
### Flag
`CTF{d8675fca837faa20bc0f3a7ad10e9d2682fa0c35c40872938f1d45e5ed97ab27}`