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.