It's in a similar vein as the variant I developed, which makes you declare that you are in a situation that requires a guess. I don't use an SAT solver, and I prepopulate the board.
https://magnushoff.com/articles/minesweeper/
In comparison to the Simon Tatham version mentioned at the end of the article, my game allows all game configurations while Tatham's version guarantees solvability by restricting the possible configurations.
Under the "Complete solution: Global reasoning" section, you say that the situation requires accounting for the entire game state - but I think my solver can do it without resorting to that?
Given
. a
.2 bX
.22 as cYZ
.... defg
(X:) `abc` contains 2 mines.
(Y:) `bcdef` contains 2 mines.
(Z:) `def` contains 2 mines.
Which can be combined:
(X-a:) `abc` contains 2 mines so `bc` contains between 1 and 2.
(Y-(X-a):) `bcdef` contains 2 and `bc` contains between 1 and 2 so `def` contains between 0 and 1.
(Z-d:) `def` contains 2 so `ef` contains 1-2.
((Y-(X-a))-(Z-d):) `def` contains 0-1 and `ef` contains 1-2 so d contains 0 mines and can be cleared.
Have I missed something? Let me know if I haven't explained it properly.
Right off the bat, I cannot agree that abc must contain exactly 2 mines. From what we can see, abc contains _at most_ 2 mines. There may or may not be mines in what you have left out, and we cannot know without considering what's there.
I haven't written a formal proof for that statement, but I have been unable to solve it to my own satisfaction by reasoning about a reduced view of the board.
.--- a---
.2-- bX--
.22- as cYZ-
.... defg
. means unknown
- means clear (and in a real game would reveal a number and therefore a constraint, but we don't need to consider those numbers for this solution)
a number means clear and producing a constraint that we want to use
This mirrors the game state in the article, and would allow us to assert that abc contains exactly 2 mines, while still only having to consider a 4x4 section of the board.
Thanks for helping me with this btw, it's much appreciated :)
This is in contrast to the local rules I first describe that consider only a very limited part of the board, and there is a pre-determined hard limit for how much would ever need to be considered for these rules.