[maggit]

Great read!

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.

[StevenWaterman]

I'm currently writing a minesweeper solver in my spare time and have a question about one section of your article.

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

Then we have the constraints:

(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.

[maggit]

It's been some years, but I think it boils down to the definition of when you are _considering_ some part of the game state.

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.

[StevenWaterman]

Sorry, I left out some bits of the game state for conciseness - perhaps this is a better way of displaying it

    .---       a---
    .2--       bX--
    .22-  as   cYZ-
    ....       defg

Where:

. 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 :)

[maggit]

Right, so, in my book, reasoning based on facts such as "these squares are clear" are _considering_ those squares.

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.