Oh hello minesweeper. It's been a while since I last talked about it even though this is something I never left it up on the shelves: I showed up playing MSN minesweeper at times (perhaps once a year), and tried minesweeper speedrunning at times but those were nothing new.
What caught my attention is a new minesweeper like mobile game where you fill the tiles by colors. This is immediately a variant of minesweeper with the following rules:
- Colors: there can be 2, 3 or 4 colors, but let's assume we are talking about the 2 color version for simplicity since it is then equivalent to OG minesweeper.
- Difficulty: either basic or advanced.
Basic: you should be able to find tiles that solve directly. For example if you see a red-2 but there are already 6 non-red neighbors (either colored non-red or marked non-red), then you know the remaining two much be red.
Advanced: Only guarantee logical solving.
- Extra rules: some of the games are coupled by extra rules like number of tiles/chained blocks of a certain colors of a row/column, number of 2-chains on a row/column, symmetry, dominant color of a row/column...etc
Every game is composed of a color rule, basic/advanced rule set + optional extra rules and should be solvable logically.
As a minesweeper veteran you would find the basic rule set extremely satisfying to play since everything can be processed quickly. 30 seconds to solve a 8x8 board is almost routine.
However, some of the extra rule set isn't that simple yet it could appear together alongside basic rule set. Consider symmetry rule for example: instead of numbers, some tiles are filled with -> <- arrow pairs, indicating palindrome pattern between arrows.
One expected operation for symmetric rule is the ability to deduct the position of the ending arrow given a starting arrow and a few colored tiles in between. But such deduction does not sound simple at all right?
Despite how the game handles such conflict, we ask an important: how to properly define simple-ness?
And then there comes the advanced rule set.
In the tutorial the following example is given:
2 □ □
x □ 2
(□ = unrevealed tile, x = mine)
Tutorial used that as an example of 'non-simple' logic: if the right top corner is safe then we have to flag both tiles on column 2 violating the 2 at left-top corner. Thus right top corner must be flagged.
I read the whole thing in a different way though. Instead of treating it as a propositional logic problem, I see it as an linear integer programming problem. In plain terms I am looking to deduct using equations.
In the above example let us encode as
2 A C
x B 2
That gives A+B=1 and A+B+C=2 which solves to C=1.
Such approach is nothing new and I believe many are doing the same. In fact, I found this approach almost universal, meaning I can solve most problems simply using such counting trick, but is that true?
The problem here is, assuming the board is logic-solvable can we use equations derived from hints to find the answer?
Simple board
It's so hard to define what a simple rule set is, especially when it is mixed with other extra rules. But what if we separate what we can do per rules?
Define operations allowed under "basic rule set" as follows:
1. If #neighboring mines = mine number, mark all remaining neighboring tiles safe
2. If #remaining neighboring tiles = #remaining mines, mark all remaining neighboring tiles mines
We can do the same for any extra rules. Take "number of mines in a row/column" as example the rules could look like:
1. If #mines on row/column = mine number, mark all remaining tiles on row/column safe
2. If #remaining tiles on row/column = #remaining mines, mark all remaining tiles on row/column mines
Those rules could be a lot more complicated for other rules though. Imagine the rules about number of chains on row/column...
These set of operations are essentially logical inference theorems. That says, a logically solvable board is a (finite) board that at each state there is at least a tile that can be marked either safe or mine using one of the theorems.
Advanced rule set
Ok then what separates from the basic rule set then? In the above example we see that those operations is simply not enough. In fact we know that if we have finite (or polynomially many) rules, each rule has polynomially many scopes to check, each application is in P and a search invokes the rules polynomially many times, it would not be a logically complete search.
That is unless, of course, if P equals NP (equals coNP) (!!!).
NP-completeness is proven by showing circuit-SAT reduces to minesweeper. In other words we actually have a construction of boards from logically hard problems. That says, the approach of producing a set of quick rules won't get you anywhere.
When (polynomial time) inference approach does not work anymore, the only thing we can do is to rely on the existence of solution. We can define an operation like:
1. Mark a tile safe/mine, if all possible solutions from current board state have that tile marked safe/mine.
That's pretty much it. The universal definition of solvability in one sentence, although it doesn't mean simplicity at all. Check all solutions is an exponential approach. Although the fact that propositional logic is complete means there will be a deduction from the current board if there is possible progress, but at what cost can we find the deduction? I guess you know better unless a certain equality is miraculously true again ;)
In some sense basic vs advanced is just a disguised P vs NP just like 2-SAT vs 3-SAT*.
Logical deduction vs mathematical formulation
This is another issue that looks unrelated to the above but just look at how all previous talks were focused on NP-completeness and SAT solving, how could this be an exception?
On the logical side, minesweeper is obviously a SAT problem.
On the mathematical side, it isn't just a linear system -- it's a binary system where all variables must be 1 or 0.
The fact that all variables must be below 1 and above 0 is surely well understood as this is precisely how the basic operations work, but this is nothing spectacular. A linear system with inequalities are merely linear programs with well understood properties and polynomial algorithms. Integer programming on the other side, is a completely different beast.
We constructed an example where integrality matters:
x x 4 x x
x F x D 4
4 x x C B
A x 7 x x
2 E x x x
This is a typical successive either-or pattern. Each consecutive pair in the chain D-F-A-E-C sums to 1 like A+F=1, F+D=1 and so on. The caveat is the head and tail are connected here and is bounded by the extra equation B+C+D = 2.
Since we know A=C=D we substitute to get 2A+B = 2, so integrality forces (A,B) = (1,0). In logical terms, the cycle forces C and D to be either both safe or both mine but since there is at least one mine among C, D we conclude both must be mine. This would never be solved without quoting the integrality constraint.
Although all the above merely give you a feel on how minesweeper is actually a subproblem of 0-1 integer linear programming (ILP), it's still far from a complete proof that it is NP-complete. Can we reduce any 0-1 ILP problem into minesweeper board? This is actually very tricky because it is almost impossible to corporate large coefficients in minesweeper board given its geometry. That's precisely why the actual proof took the alternative track by showing circuit-SAT reduces to minesweeper in the logical sense instead, which makes Karp happy.
Nonetheless, it is much easier to prove that the universal theorem from the logic side is equivalent to the universal theorem from the math side. We may as well define the operation in the mathematical way:
1. Mark the tile $X_i = 0/1$ if every solution vector $x$ to the system satisfies $x_i = 0/1$.
That says, if you take things to the extreme and consider the complete power of logical solving and mathematical solving the two are equivalent. It will likely be all we will know unless someone start to ask question like "can we compare the strength of a set of operations in solving ILP and a set of inference rules in logical deduction?".
For example, consider the LP relaxation $\left\{ Ax=b, 0\leq x_i \leq 1\right\}$. This is surely P-time solvable. What is the corresponding logical inference rules? The answer is surprisingly clear with the help of Farkas using duality. The unfortunate bit is that the inference rule basically looks so mathematical where we start to lose the boundary between 'logical' and 'mathematical'.
***
This minesweeper variant got me to think a lot about mathematics behind, but the deeper I go I realized all of them reduce to the basic principle of completeness with basically nothing more. Let's call it a good revision and look over it.
There is an important take away though. Logical approach and mathematical approach are deeply entwined. The deeper we try to look into, the close the they look. Instead of treating the two separately, we should learn to make use of both: we use the logical approach to perform reduction, and we use the mathematical approach to understand its formulation. Minesweeper becomes a beautiful medium where the two meet, and I hope you can appreciate it too :)
(*): to be precise this is not the most accurate comparison as inferences and solvability is coNP-complete not NP-complete but you get it.
