[dmurray]

Agreed, I'd like this to go one step further and allow you to guess on a square where you will inevitably have to guess anyway.

I'm not sure how hard this is to add to the SAT solver. The formal definition is something like "if for some set of maybe-squares S, no matter what the solutions are to all of the squares outside S, the set of solutions to S is the same, then allow clicking anywhere in S". But that's a combinatorial explosion: just the number of sets S to consider is a factor of 2^#{maybe-squares} . I don't know enough to say if that can be optimized into something sane so that it can be rigorously applied, but a handful of special cases for small unconnected sections of the board would cover most of it.

[reificator]

> I'd like this to go one step further and allow you to guess on a square where you will inevitably have to guess anyway.

If you have all of the possible information for that guess already, then yeah.

If there are still some unknowns that you could resolve first to get more information, then guessing should still result in a mine.

[dmurray]

Yeah, that's what I meant really, as per my attempt to formalize it.

I can't think of any situations where it makes a difference, though, other than ones where you rely on the mines-remaining counter.