Comment by npinsker
2 days ago
For what it's worth, the way 14MV does hints is probably by just throwing the board into Z3 (https://github.com/Z3Prover/z3) or some other constraint solver. Microsoft has already done all the hard work for you.
2 days ago
For what it's worth, the way 14MV does hints is probably by just throwing the board into Z3 (https://github.com/Z3Prover/z3) or some other constraint solver. Microsoft has already done all the hard work for you.
I doubt it. A guaranteed-solveable minesweeper scenario isn't just about the global board setup, but about what information is available when, and what order the solution is gone through.
Bombe[0] is to my mind the definitive exploration of this concept. The tagline is "Minesweeper, but you only solve each situation once", which you do by writing these kinds of deduction rules with a fairly painful visual programming language. (You can't write an invalid rule: the game will detect the logic error and present you with a counter-example.)
You then let the computer churn through it's list of 100k scenarios idle-game style, until you bump into a board that can't be solved with the rules you provided, and you have to figure out what new rules to write.
As the game progresses, you'll unlock ways of parameterizing the rules in various ways, as well as various variant rules.
[0] https://store.steampowered.com/app/2262930/Bombe/
You're right, I misspoke a little bit -- 14MV is able to do this because (unlike this game) it does not reveal all givens to you at the beginning.
Bombe is easily one of my favorite games ever. 240+ hours of gameplay so far.