Cracking Minesweeper with Z3 SMT Solver | Hacker News Reader

Cracking Minesweeper with Z3 SMT Solver

yurichev.com

177 pointsiou56 comments

I 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/.

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

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

How does this contrast with Answer Set Programming (using e.g. clasp)?

They 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

Sudoku examples: SABR: http://www.hakank.org/sabr/sudoku.tb

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

Here we go again. Someone says "minesweeper". I shamelessly plug my js implementation: 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.

Nice :) - FYI though with Chrome on macOS marking a flag works, but also opens the context menu.

Looking 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!

Nope, console was closed. But going back to it, it's fine now! Very strange.

(The game state saved in local storage, very nice :))

The delay in the click sound is so annoying.

Edit: only delayed in Safari.

This was my first try: http://imgur.com/a/EQsm8

I guess I should not buy lottery tickets today

I got a bomb on my 2nd random click.

Just an interesting tidbit - you can't bomb (bug) on first click. If you hit one, the board is reshuffled so that your first click is good. Apparently this fantastic UX feature was part of the original game. When someone pointed that out first time I posted it here - I just had to add it.

Every time I read a minesweeper article I let my browser autocomplete "mines" to go to your program. Thanks for making it!

Hmm, I seem to hit corner bugs a lot but in minesweeper the corners never had mines (which was like the whole initial strategy)

Corners in minesweeper always had the same chance as any other square to be a bad choice even the example in the main article shows a corner mine

I've got one too [1]. Your's looks much nicer than mine. I'm just an occasional dabbler in JavaScript, so it is not surprising that mine is crude.

I wrote that after reading this HN discussion [2] where someone was describing how they interview. They set the candidate up with a good JS development/test environment that the candidate is comfortable with, and ask them to implement as much of Minesweeper as they can in one hour. They also said no one has ever finished in that one hour.

As expected, I did not come anywhere near doing it in an hour. Wall time was about 7 hours, but I was doing other things during that, so it was about 4 hours working on Minesweeper. About an hour of that was testing and stumbling around the Mac character viewer trying to find good characters for bombs, flags, and such.

I'm kind of surprised no one has done it for the interviewer in an hour.

As I said I'm only a JS dabbler. Basically, every couple of years or so I'll have to do a little bit of basic JavaScript to do some simple DOM manipulation or form validation. That's just enough to keep me sufficiently aware of JS that I can at least do some reasonable guessing and googling.

I'd expect an actual JS programmer to be much faster than me.

[1] https://github.com/tzs/interview_minesweeper

[2] https://news.ycombinator.com/item?id=10752564

I think I'd panic if I got that question in an interview. Where do you start with that? What are the first steps? How did you know what to Google?

It sounds like a test of your ability to abstract, componentize, and prioritize. Here's a possible approach to this sort of problem:

Read a brief summary of whatever you are implementing, even if you are already familiar. This will help you understand the breadth of the problem.

Try to list in very broad terms the data structures you will need to store the state of the problem (e.g. for Minesweeper, a grid of tiles, and for each tile some status). Don't worry about whether you are using a list or a vector/array or sparse or dense matrices, just be as generic as possible.

List in very broad terms the logic of the problem. What states exist, what are the beginning/ending conditions (start/playing/win/loss), very roughly how states transition, etc. Again, avoid detail.

Identify the inputs and outputs of the problem, very broadly (e.g. user input, display for game board -- no mention of mouse, keyboard, HTML, or whatever).

Cycle through these phases a few times until they seem to agree.

From there, go wherever your brain takes you, progressively filling in details of your design. You probably still shouldn't start coding.

For a 1hr exercise, let's assume you've used 15 minutes for the design phase. Now you can begin coding. Start with the very core of the problem, writing data structures and logic around those data structures. Then get some way of displaying them and manipulating them so you can debug with feedback.

With a roughly functioning core, start filling in the rest of the design. Focus on what makes the biggest functional difference with the least effort first, if at all possible, but again, follow your brain. Try not to pick fonts before you've got everything running. Go piece by piece, until time is up.

As for what to Google, you'll need to know how to interface with your problem's input and output systems (like a browser), and maybe how to run timers or store your particular data structure, but most of the work is design, not research.

For a personal story, several years ago I failed a similar test in an interview. They asked, "How would you make an elevator?" I got lost in the details like what type of screw terminal to use for electrical contacts, and only later realized the value of prioritizing layers of abstraction. Breadth-first search, not depth-first, if you think of a problem space as a graph.

I just tried a version of this as a test for myself. I was able to create a very serviceable minesweeper clone in pygame, finishing up at almost exactly the 1 hour mark.

I didn't have time to include a game-over animation, an in-game timer, or a way to select different settings, but the core mechanics were all there.

Pygame is a very nice environment for games programming when you want to do something fairly simple.

I'm the same way with my solitaire game!

https://solitaire.gg

We should build a collection of web remakes of the built-in OS games.

that page is blank unless you allow ajax.google.com....

That's like half of the internet these days.

Probably not half, but way too much. I'm hoping that the recent Amazon downtime will help put the breaks to this trend.

I pointed this out before the last time you plugged your implementation.

It has a bug in it. If you right click (place a flag) then right click (remove that flag) then left click, it places a flag instead of revealing.

I fixed it. Now, there are no known bugs.

You ratbag, you just cost me 10 minutes. :P

Nice implementation though. :)

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

It's very simply provable that there exist configurations you must guess in, even if weighted.

It'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/

The 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?

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

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

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

Some games do this, some don't some only actually generate the field once you click the first box.

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

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

Oh, 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)

It was definitely not like that on Win98.

Definitely not like what the parent said, or what I said? Maybe I'm remembering that rather than XP

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

Consider 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

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

Not for normal minesweeper, but there are always-solvable variants: http://www.chiark.greenend.org.uk/~sgtatham/puzzles/js/mines...

I'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.

There's a minesweeper solver which works out all the probabilities of uncertain squares. http://mrgris.com/projects/minesweepr/demo/player/

The creator wrote an explanation here: http://mrgris.com/projects/minesweepr/

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

I 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."

No. some configurations can be solved perfectly but as you get to higher mine density it becomes probabilistic.

There 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

I wrote a Minesweeper solver a while ago, it uses backtracking search with decent results: 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?

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

The thing is that in minesweeper you cannot win in a deterministic way. Sometimes you will lose in your first move.

I 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 ;)

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

There'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

Great project! Made me remember making a Fallout 2 Computer Console cracker in Perl. Great fun!

I don't remember any hacking in FO2 (at least, not minigamed).. Do you mean 3?

Reply on news.ycombinator.com