Playing Minesweeper with Z3

SAT solvers can take in any boolean formula, like the following, and return whether there is at least one assignment of variables that satisfies the formula. If there is such an assignment, the formula is satisfiable, or SAT. If not, it's called UNSAT¹. $$(x_1\wedge\neg x_2)\vee x_2 \wedge (x_3 \vee \neg x_1)$$

SAT is an NP-Complete problem, which means two things:

1. we don't know of any algorithm that can solve it quickly (=polynomial time), but we can quickly verify whether a given solution, such as an assignment of variables, is a real solution.
2. All other problems in NP can be converted to SAT quickly.

In practice though, we solve SAT and other problems in NP all the time using heuristics that work well most of the time. And there's been a ton of work done to make SAT solvers really fast.

And this means we can take a lot of other thorny problems and use the efficiency of SAT to help solve them. One somewhat general purpose solver that uses SAT heavily is Microsoft's Z3 SMT solver.²

SMT stands for Satisfiability Modulo Theories, where theories are kinda like extensions to the typical SAT paradigm that allow the solver to deal with variables beyond booleans and constraints beyond propositional boolean logic.

One common use case for Z3 is program analysis, where it's used to ex. determine if it's possible for something to error (where the constraints come from the control flow conditions, variable assignments). This is called symbolic execution.

Instead of doing symbolic execution, I'm going to use Z3 to play Minesweeper. Minesweeper is a good problem for a solver as a lot of the time it's unambiguous whether a certain square can have a bomb below it or not, but it sometimes takes a fair bit of reasoning.

The game of minesweeper consists of an $n\times n$ board, of which some squares have bombs hidden underneath. The goal of the game is to find and place a flag on all of the bombs. Digging a square without a bomb under it will reveal the number of bombs within the $8$ neighboring squares.

Here's the approach I'm thinking of:

• Each square gets a boolean variable that represents whether it has a bomb. This gives us $n^2$ variables.
• For each numbered square, add a single constraint that encodes "of my $8$ neighboring squares, exactly $x$ have bombs", where $x$ is the revealed number.
• For each dug square, set it to false (no bomb there).
• maintain a queue of the frontier squares. For each turn, look at each square in the frontier:
  • Set that square to true (deciding that it's a bomb). Run the solver; if that's UNSAT, there can't be a bomb there and we can dig it safely. Then we can roll-back that constraint, returning from our hypothetical world.
  • When we dig a square, it exposes one or more squares, allowing us to add more constraints.
  • Else, force no-bomb. If that's UNSAT, there must be a bomb there and we should flag it.
• Repeat ^ until all bombs are flagged³

I had claude write me a simple Minesweeper using pygame, and installed the python bindings for z3.

I created a Solver instance and set up my variables:

from z3 import *

# ...uninteresting code here...

solver = Solver()
is_bomb = [[Bool(f"{r}-{c}") for c in range(NUM_COLS)] for r in range(NUM_ROWS)]

To add constraints for a revealed square, we can make use of the Pseudo-Boolean Equality (PbEq) constraint, which constrains a weighted sum of booleans to equal a constant. In this case, we set the weight of each boolean to $1$, as we just want to equate the total number of true booleans to the revealed number.

def gen_constraints_for_revealed_square(r, c, num_revealed):
	is_not_bomb_constraint = is_bomb[r][c] == False
	adjacency_constraint = PbEq([(is_bomb[nr][nc], 1) for nr, nc in neighbors(r, c)], num_revealed)
	return is_not_bomb_constraint, adjacency_constraint

Under the hood, this constraint gets converted directly into a boolean formula to be fed to the SAT solver. Another way to encode the constraint would be:

adjacency_constraint = sum([is_bomb[nr][nc] for nr, nc in neighbors(r, c)] == num_revealed

This causes the booleans to be treated as true integers equal to $1$ when true and $0$ when false: If(bool, true_val=1, false_val=0), and adds an equality constraint with num_revealed. Instead of being converted directly to SAT, these constraints would be handled by the linear integer arithmetic theory. I think it's faster to use PbEq in this case to avoid the overhead of the solver going back and forth between the SAT solver and the arithmetic solver.

First dig and adding initial constraints:

safe, revealed = game.dig(4, 4)
for r, c, val in revealed:
	solver.add(*gen_constraints_for_revealed_square(r, c, val))

And the core loop:

frontier = deque(game.get_perimeter())
while True:
	while True:
		r, c = frontier.popleft()

		solver.push() # checkpoint constraints
		solver.add(is_bomb[r][c] == True) # hypothetical: bomb under square
		if solver.check() == unsat:
			safe, revealed = game.dig(r, c)
			assert safe

			solver.pop() # undo hypothetical

			for nr, nc, val in revealed:
				solver.add(*gen_constraints_for_revealed_square(nr, nc, val))
				for neighbor in neighbors(nr, nc):
					if neighbor not in frontier and not game.is_revealed(*neighbor) and not game.is_flagged(*neighbor):
						frontier.append(neighbor)

			break
		else:
			# possible for a bomb to be there
			solver.pop() # undo hypothetical

			# MUST there be one?
			solver.push()
			solver.add(is_bomb[r][c] == False) # hypothetical: no bomb under square
			if solver.check() == unsat:
				# yup - flag it!
				game.flag(r, c)
				game.render()
			else:
				frontier.append((r, c)) # look at this square again later when more is known
			solver.pop() # undo hypothetical

And it works!

Stuff I'd like to look more into

• Programming Z3 looks like it has a bunch of good info on how Z3 handles theories under the hood.
• What are other cool things you can use an SMT solver for?
• What's the shape of problem that you should reach for this as opposed to fully converting something to SAT or using a CP(-SAT) solver?