Group members: Christopher Du, Iris Liu, Iman Moreira, Juniper Parsons, Zibing Zhang
This post will describe the reduction of playing* a game of Minesweeper to solving the all-solution Boolean satisfiability problem (AllSAT).
*It is important to realize that Minesweeper is not a game with perfect information, while SAT is a "game" with perfect information. Therefore it is not exactly possible to reduce the playing of Minesweeper to solving ALLSAT. However, for each individual move, it is possible to reduce that decision problem to ALLSAT.
Minesweeper is a single-player, puzzle video game in which the player has to "clear" the board without detonating any of the bombs.
This post will focus on the version of Minesweeper that was bundled with Windows 7. For anyone interested in playing the game, an installation can be found here. Another version of the game can also be found online here.
The goal of the game is to clear the entire board without detonating any bombs. After the first move, an area of the board is initially cleared. Inset tiles have been cleared, while raised tiles have yet to be cleared, or may contain bombs underneath. The number displayed on a cleared tile indicates the total number of bombs on its adjacent tiles. Blank tiles are not surrounded by any tiles.
The player is able to flag tiles they believe to contain a bomb. The player must methodically click on raised tiles to clear them.
The game is over once all tiles that do not contain bombs have been cleared, or once the player clears a tile that contains a bomb.
For any Boolean formula, the Boolean satisfiability problem is the problem of determining if there exists an assignment of the Boolean variables such that the formula evaluates to TRUE. SAT is famously known to be NP-complete.
Developing state-of-the-art SAT solvers is an active area of research. Most modern solvers rely on assortment of techniques such as conflict-driven-clause-learning and the Davis-Putnam algorithm.
There are two basic strategies that can be used to progress the game to an advanced state. Eventually, we must rely on a reduction to ALLSAT to progress further into the game.
Consider the situation above which occurs in the upper right hand corner.
The cell in the upper right hand corner indicates that there is exactly 1 mine in its adjacent cells. Since there is only 1 uncovered adjacent cell, the uncovered cell must be the mine, and so we can flag that cell.
The cell to the left of the cell in the upper right hand corner indicates that there is exactly 1 mine it its adjacent cells. Since we know the cell below it must be a mine, all other surrounding cells can safely be uncovered.
The 1-2-1 pattern is a very common pattern.
Most players should know immediately that the solution is to flag cells
For the simplicity of the reduction, we will only focus on the middle three cells. For each cell, we will use their surrounding, uncovered cells to create a boolean expression that describes their relationship with each other. Finally, we will combine the three expressions into a single expression and apply SAT on the combined expression.
Each cell is labeled with a boolean variable,
Consider the second cell from the top.
We know that exactly one of
Consider the third cell from the top.
We know that exactly two of
It is clear that the fourth cell from the top mirrors the second cell from the top. Combining the three boolean expressions for the middle three cells, we have the combined boolean expression.
Running the expression through a SAT-solver, we can see that
TODO: talk about ALLSAT, how multiple solutions creates ambiguity, but how we can use number of solutions as a heuristic as to how to proceed in the game