Minesweeper pt. 2: SAT (the cheating button)

Previous:

• Minesweeper Turbo

In the previous post, I applied some more or less simple rules for playing Minesweeper. At the end of it, two issues were raised. First, we would like to generate only problems that we know are solvable. Second, we would like to check whether a certain situation is truly "impossible", or whether we can make more inferences. Both of these features would be simple if we could automatically exhaust all possible inferences for a certain board. This is what SAT will do for us. 

Implementation

The method of determining whether or not tiles are mines will be proof by contradiction. We will set up a SAT model that holds the adjacency constraints. A tile X can be shown to be a mine by showing that "X is free" leads to the SAT model being unsatisfiable. Likewise, X can be shown to be free by showing that "X is mine" makes the SAT model unsatisfiable. 

Aside from the adjacency constraints, we can also add a global constraint on the total number of mines, since this is known to the player. 

For performance reasons, the only unknown tiles considered will be those that touch an open tile. None other are relevant for the adjacency constraints. 

	# The class of 'self' inherits nx.Graph
	def apply_SAT(self, board):
	while True:
	# Let the trivial rules do the heavy lifting,
	# for speed.
	self.apply_trivial(board)
	solver = SugarRush()
	known_tiles = set([tile for tile in self
	if self.nodes[tile]["mine"] is not None])
	known_dilute = set(flatten([self[tile] for tile in known_tiles]))
	# The rim consists of unknown tiles that touch known tiles.
	rim = known_dilute - known_tiles
	unknown_tiles = set(self.nodes) - known_tiles
	unknown_dilute = set(flatten([self[tile] for tile in unknown_tiles]))
	# The front consists of known tiles that touch unknown tiles.
	front = unknown_dilute - unknown_tiles
	# The decisions we are interested in
	# is what to do with the unknown tiles.
	tile2var = {tile: solver.var() for tile in rim}
	# Cardinality constraints.
	# The number on known tiles must be equal
	# to the number of adjecent mines.
	for tile in front:
	if self.nodes[tile]["adj"] is None: # mine
	continue
	unknown_neigh = self.get_unknown_neigh(tile)
	unknown_neigh = [tile2var[neigh] for neigh in unknown_neigh]
	adj = self.nodes[tile]["adj"]
	flagged_neigh = self.num_mine_neigh(tile)
	remaining_mines = adj - flagged_neigh
	solver.add(solver.equals(unknown_neigh, bound=remaining_mines))
	# Global constraint
	# The total number of mines is known,
	# so we can add a constraint for this too.
	all_vars = [var for var in tile2var.values()]
	remaining_mines = self.S - self.num_mines_total()
	if len(rim) == len(unknown_tiles):
	solver.add(solver.equals(all_vars, bound=remaining_mines))
	else:
	solver.add(solver.atmost(all_vars, bound=remaining_mines))
	for tile in rim:
	# Do reductio ad absurdum on tile values.
	var = tile2var[tile]
	if not solver.solve(assumptions=[var]):
	# Assumption that it's a mine failed -
	# must be free.
	self.sweep(board, tile)
	# New information: go through all unknown tiles again.
	break
	if not solver.solve(assumptions=[-var]):
	# Assumption that it's free failed -
	# must be a mine.
	self.flag(tile)
	# New information: go through all unknown tiles again.
	break
	else:
	# Could not infer any new tiles: exit.
	break

view raw ms_sat.py hosted with ❤ by GitHub

Consequences

Given a method to exhaust all inferences, we can generate solvable instances by running the apply_SAT function to the initial state, and see if it leads to a finished game. If not, generate a new problem and try again. When we are working with a solvable game, we always know that there is at least one way to proceed, at least one tile that can be inferred to be free or a mine. 

For games that are not guaranteed to be solvable, I installed a "cheating button". We can also call it an "answer sheet button". The cheating button runs apply_SAT. If no more tiles open, the situation was actually hopeless.  If some tiles opened, there was something to do. After apply_SAT finishes, however, there is nothing to do. One must simply take a guess. Of course, in Minesweeper we do not care to guess, so mathematically, the game is over. 

Performance

Proving that a given Expert game (16x30 tiles, 99 mines) is unsolvable takes 0.1-1 seconds. Proving that it is solvable is about the same. For a Super-Expert game (30x50 tiles, 300 mines), the time is about 1-10 seconds for proving solvability/unsolvability. Expert games and Super-Expert games are solvable with a rate of about 1 in 10.