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. 

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.