7 ms·
Cracking Minesweeper with Z3 SMT Solver
- iaw 10y agoThis makes me wonder: Is there a strategy such that it can consistently solve every minesweeper configuration? I always assumed that the 50/50 guess was unavoidable on some maps but I don't know if that's true.
- drchickensalad 10y agoIt's very simply provable that there exist configurations you must guess in, even if weighted.
- mod 10y agoIt's not possible, no. The guessing is not a part of every layout, but often it is. See the board positions in this blog post: http://nothings.org/games/minesweeper/ http://nothings.org/games/minesweeper/
- inlined 10y agoThe proof seems pretty easy to reduce with a smaller example: there are 17 mines. One cluster is in a 3x3 box and another is in a hollow 3x3 box. Which is which?
- Pxtl 10y agoConsider the basic state - the minesweeper board is built around your first move. If your first move is not a void, but has one or more adjacent mines, all you see to start is a single open square with a number. At that point you're already making a guess. Even if it's a 1, you're guessing about your next move.
- saghm 10y agoNot to mention that the first move itself is a guess. I'm not sure about all variants, but certainly on the classic Windows minesweeper there were times that my first click was a bomb.
- nicholaides 10y agoYou would think that if you clicked a bomb first, the app would regenerate the board until it made one where the place you clicked was not a bomb.
- ATsch 10y agoSome games do this, some don't some only actually generate the field once you click the first box.
- ygra 10y agoThe behaviour towards the user is the same, though: The first click never results in a bomb. Everything else is an implementation detail, although not placing bombs until after the first click is probably the easiest approach to ensure it.
- M4v3R 10y agoThat was definitely not possible on Windows XP version of Minesweeper, they would regenerate the board if you clicked on a bomb in the background and used that one instead.
- saghm 10y agoOh, really? I guess I was just misremembering things. Thanks for correcting me here! (not sarcastic, genuinely happy to be corrected when I remember things wrong)
- Drdrdrq 10y agoIt was definitely not like that on Win98.
- saghm 10y agoDefinitely not like what the parent said, or what I said? Maybe I'm remembering that rather than XP
- iaw 10y agoI was thinking that past a certain threshold of moves the probability of clicking a mine in most strategies will drop to zero, the question I had was if there were a specific strategy where that probability would never increase past 0. From all the commentary however, it's pretty clear that the answer is no.
- derf_ 10y agoConsider the following configuration (where --- is the wall and M == known mine): +------ | 1 | 2 | 1 2 M If you know there are three mines here, including the marked one, this is either +------ | M 1 | M 2 | 1 2 M or +------ | M 1 | M 2 | 1 2 M There's no way to ever get more information to resolve the ambiguity without guessing, and the mine probability in every square is 50%. This (or simple variants) is the most common late-game failure case. Similar symmetries can also occur on edges, and (though more rarely) even in the middle of the field. If you assume that you have knowledge of the 5 outside squares of a 3x3 corner (and any neighbors outside of that 3x3 corner) and that you know how many mines are left, you won't be able to fill in the rest without guessing 4.14% of the time on an Expert board. The most common failures are either three three-mine cases like the one illustrated here (0.440% likelihood each) or one of 16 four-mine cases (0.115% likelihood each). Given that there are four corners on the board, that sends your failure rate to at least 15.572% (actually higher, because you don't always know how many mines are left in one corner without clearing the other three). If you want to fail fast, figure out if you have symmetry in the corners first.
- mhils 10y agoNot for normal minesweeper, but there are always-solvable variants: http://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/mines.html http://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/mines...
- ballenf 10y agoI'm sure someone's maxed the strategy, but playing I would always try to figure out when I got to those forced-guess situations which click had the lowest probability of being a mine. I.e., there were squares that you knew were 1/2 or 1/3 chance, you knew how many total unrevealed mines and number of unrevealed squares. So you could calculate the odds on any given square. One of those problems I always wanted to work on on my own, knowing that someone somewhere probably had a much better solution.
- Hussell 10y agoThere's a minesweeper solver which works out all the probabilities of uncertain squares. http://mrgris.com/projects/minesweepr/demo/player/ http://mrgris.com/projects/minesweepr/demo/player/ The creator wrote an explanation here: http://mrgris.com/projects/minesweepr/ http://mrgris.com/projects/minesweepr/
- i336_ 10y agoThis implementation shows you where the mines are! This will be so useful for actually helping me understand how Minesweeper works - theoretical explanations just make my eyes glaze over more often than not.
- jmtame 10y agoI think it would depend on a few things: the size of the grid, how many bombs there are, and whether the board uses the rule of "the first click is guaranteed not to be a mine."
- orasis 10y agoNo. some configurations can be solved perfectly but as you get to higher mine density it becomes probabilistic.
- kmod 10y agoThere are a couple questions here: - Can every minesweeper board be solved without guessing? No: 1 ? 1 ? - If a minesweeper game doesn't require guessing, is there an algorithm that can determine the next move? Yes. Just enumerate all combinations of mine/not-mine for every hidden cell, and look at all the boards that match the exposed clues. If there is a square that is never a mine, click it. If there isn't, the board requires guessing. - Is there an efficient algorithm to do the above? Most likely not. Minesweeper as a decision problem ("is there any solution to these given clues") is NP-complete. http://simon.bailey.at/random/kaye.minesweeper.pdf http://simon.bailey.at/random/kaye.minesweeper.pdf
- dino463 10y agoI wrote a language some time ago exploring the use of SAT solvers for these types of problems, trying to make writing solvers easy to reason about, never quite took off, but here's what the minesweeper solution looked like: http://sabrlang.org/mine/ http://sabrlang.org/mine/. It basically translates the somewhat more complex rules into the simpler SAT rules using minisat. However sometimes needed a generator in python to make the rules :/. But still kinda nice to see it more visually, language looks like this in the end: http://sabrlang.org/code/mine/source.txt http://sabrlang.org/code/mine/source.txt. It basically lists the requirements for middle, edge and corner blocks, than says where those blocks are on the "board." Kinda fun, though arguably somewhat restrictive. One of the more fun ones I think is the rubiks cube: http://sabrlang.org/rubik/ http://sabrlang.org/rubik/.
- cscurmudgeon 10y agoLooks awesome. Went through a few examples. You should do a post on HN. Planning on exploring more when I have some free time after a few weeks.
- rw 10y agoHow does this contrast with Answer Set Programming (using e.g. clasp)?
- dino463 10y agoThey are similar, although SABR tends to be more verbose as it keeps a polynomial relationship between size of SABR programs and the underlying SAT. It can in some ways be easier to reason about, but that's sort of in the eye of the beholder. In the past I've prototyped simple examples in SABR then written a generator in python for the full program. Here's a great resource for those interested in constraint programming: http://www.hakank.org http://www.hakank.org Sudoku examples: SABR: http://www.hakank.org/sabr/sudoku.tb http://www.hakank.org/sabr/sudoku.tb ASP: http://www.hakank.org/answer_set_programming/sudoku.lp http://www.hakank.org/answer_set_programming/sudoku.lp There's the built in construct of transitions which isn't in this example that is preloaded into SABR, but one could easily enough write the restraints required for this in clasp. SABR envisions the universe as the "Board" and it has a given size consisting of elements and each element can have a specific state as defined by "Symbols". Then you can build on that to say what is legal for a theoretical set of elements, and how that set can transform over time, then you can define which of the Board elements correspond to the defined theoretical set. Its way more opinionated than most other constraint programming languages, which can be mind bendy.
- deleted 10y ago[deleted]
- luckyt 10y agoI wrote a Minesweeper solver a while ago, it uses backtracking search with decent results: https://luckytoilet.wordpress.com/2012/12/23/2125/ https://luckytoilet.wordpress.com/2012/12/23/2125/ Now I wonder how does the performance of this SAT solver compare to backtracking? Which one deals better with situations where guessing is required?
- amluto 10y agoIn Stanford CS221, one of the assignments was to write a Minesweeper solver using backtracking and various propagation techniques. It was exact and ran fairly quickly. Once you've enumerated all possible solutions, you can throw heuristics at guessing.
- ronilan 10y agoHere we go again. Someone says "minesweeper". I shamelessly plug my js implementation: http://www.ronilan.com/bugsweeper/ http://www.ronilan.com/bugsweeper/ Don't ask me why. P.S - it's with bugs instead of mines just because fontawesome didn't have mines. No puns intended.
- OJFord 10y agoNice :) - FYI though with Chrome on macOS marking a flag works, but also opens the context menu.
- deleted 10y ago[deleted]
- ronilan 10y agoLooking into it I'm guessing you had console open and in mobile mode (pointer is a dot). Right? In that case there is no "right-click" event in the document context. If you want console open and desktop mode, there is a little icon there to "Toggle device toolbar". Digging into Chrome tools, what a way to spend Sunday night!
- OJFord 10y agoNope, console was closed. But going back to it, it's fine now! Very strange. (The game state saved in local storage, very nice :))
- toxik 10y agoThe delay in the click sound is so annoying. Edit: only delayed in Safari.
- jontro 10y agoThis was my first try: http://imgur.com/a/EQsm8 http://imgur.com/a/EQsm8 I guess I should not buy lottery tickets today
- 10y ago
- kebman 10y agoGreat project! Made me remember making a Fallout 2 Computer Console cracker in Perl. Great fun!
- eon1 10y agoI don't remember any hacking in FO2 (at least, not minigamed).. Do you mean 3?
- doublec 10y agoThere's an implementation of a Minesweeper solver in Mozart/Oz too "Playing the Minesweeper with Constraints": https://www.info.ucl.ac.be/~pvr/minesweeper.pdf https://www.info.ucl.ac.be/~pvr/minesweeper.pdf
- partycoder 10y agoThe thing is that in minesweeper you cannot win in a deterministic way. Sometimes you will lose in your first move.
- probablybroken 10y agoI always thought it would be fun to make a version that was soluble every time by making the system reveal extra tiles as required to always allow you to continue play without guessing. I personally found the situations where half way through a large game you were forced to guess quite frustrating. Maybe deep down I just don't like minesweeper ;)
- deleted 10y ago[deleted]
- detaro 10y agoOr alternatively one that if you click a tile with the best chance in a unsolvable situation always solves in your favor, adjusting bomb locations as necessary.