Some Math about Minesweeper
Desires
An implementation of a minesweeper app that guarantees only presenting solvable games, as proven by the above algorithm
The game, traditionally
Traditionally, the game Minesweeper consists of a finite-size grid of cells, some of which are said to contain a bomb. At the start of the game, the player has no knowledge of which cells contain a bomb. The game proceeds in a sequence of turns; on each turn, the player must choose one cell to reveal. Revealing a cell has one of two effects. If the cell contains a bomb, then the game ends immediately and is considered a loss. If the cell does not contain a bomb, then that fact is revealed to the user, and additionally the user is granted knowledge of how many bombs are present in the 3x3 neighorhood around the revealed cell. (Usually this information is presented by displaying a number in the place of the revealed cell.)
Typically boms are placed randomly around the game board. This means that at the start of the game, from the player’s persective, all cells are equally likely to contain a bomb, and hence whether the first move is a loss or not is pure luck. For this reason, some Minesweeper implementations choose to defer the placement of bombs until after the first reveal in order to guarantee that the first reveal is a non-bomb. Others go further and guarantee that the first cell revealed and all surrounding cells in the 3x3 neighborhood around that cell are non-bombs.
This gives a rough characterization of “the” traditional Minesweeper game. Implementations may vary on details, such as:
Whether or not cells on opposing sides of the game board are considered neighbors; ie, whether the game board is a rectangle or a torus
Behaviour on first reveal, as discussed above.
Size of the game board, and number of bombs
Placement of bombs
Note that in this characterization we do away with the concept of flagging a cell, which most Minsweeper implementations include. The ability to flag a cell can be seen as pure user convenience and does not affect the game, but removing it makes analysis simpler.
The game, for us
A game state consists of the following data:
A valuation function taking a set of cells (often called a neighborhood) to the number of bombs we know to be present between them. Note that the domain of is not necessarily all of , since we won’t know the valuation of all sets of cells (unless the game is complete).
We could equivalently consider this function to have signature , where denotes that the valuation of a neighborhood is unkown.
A bomb function giving whether or not each cell is actually a bomb or not. The value denotes that it is a bomb, and denotes that it is not
Completeness: the goal
One goal is to present a ‘complete’ algorithm for solving a game of minesweeper, where ‘complete’ is meant in the sense that the algorithm will beat the game in all cases where no guessing is required.
To make that concrete, we introduce the following notions.
A bomb function and valuation function are said to be compatible if they do not disagree; that is, if for every neighborhood we have that is indeed the number of bombs assigned by . In other words,
This can also be interpreted as saying that ‘respects’ or ‘realizes’
Say that a cell is determined relative to a valuation function if every bomb function compatible with agrees on ; that is, if
If a turn is spent revealing a determined cell, call that a progression. Say that a game is progressable if there exists a progression. Call a game solvable if there exists a sequence of progressions resulting in a win.
Prompts
A prompt consists of a set and a valuation function . A prompt is the same as a game state but without the bomb function. The name prompt comes from thinking of it as a ‘puzzle to be solved’.
Given two prompts and , denote by their union, formed by unioning their cells and valuation functions. This is only well-defined if the valuation functions agree on .
Given two prompts and , denote by their coproduct, consisting of the cell set and the valuation function constructed from in the natural way.
Given a prompt and cells , denote by the prompt for some . This adds a new cell to along with assertions that , which states that and therefore ; ie, and evaluate equivalently.
Relative to a prompt , for a vector of cells denote by the set of valuations for those cells compatible with . For instance, if and demands that and nothing else, then we get .
Let and take a vector of variables . Assume that this vector decomposes as the concatenation , where and . Then (where is not plain cartesian product but a “zipping” cartesian product which combines pairs by concatenation)
Now need case for in
Conjecture: any prompt can be decomposed into a sequence of coproducts followed by quotients; the span of cell-vectors is the same in the original prompt as in its decomposition.
The goal here is to first show some property of the span of cell-vectors, such as that (for instance) all spans are of odd cardinality. Then we use that to show that conjunction cannot be encoded as a prompt, for instance because if we had cells such that then we’d have that is even, which contradicts that all spans are odd.
Completeness: an attempt
One attempt at a complete set of rules for solving a game of minesweeper are the following:
Unfortunately, this rule set is not complete. One counter-example is as follows:
– – – –
– 1 2 –
a b c d
– – – –
Here a number denotes the valuation of a revealed cell, and letters and hyphens denote un-revealed cells.
This valuation determines that . However, none of the proposed rules are applicable. Hence, the ruleset is incomplete.
Relation to Boolean Satisfiability
One tempting re-interpretation of the game is as a phrasing for the boolean satisfiability problem.
Given a game state, we may consider each cell to be a variable. Then a valuation corresponds to the statement that exactly of the variables in are true, which is expressible as a finite sentence. For instance, becomes
It is unclear to me at this moment whether the problem of solving minesweeper is equivalent to boolean satisfiability. While each minesweeper game can be interpreted as a boolean expression, I am unsure if the reverse is also true. Are there boolean sentences which cannot be encoded as minesweeper games?
Any sentence which conists only of conjunctions and negations (under the conjunctons), and with no repeated variables, is easy to express. Let be the set of variables, and let be the set of non-negated variables. Let . Then by split and bomb-intro we can deduce that .