👩🏼‍💼 🏩 🤶🏻 Kaboom: an unusual sapper 🧙 👏🏾 👨🏼‍⚕️

As a child, I sat at my father’s work three times a week for an hour and a half. I was allowed to go to a computer, where from entertainment there was only a sapper and Paint. I was tired of drawing quickly, but the desire to open the entire field and not explode motivated me to look for new and new ways to play this game. Many years later, I accidentally stumbled upon an interesting article about a clone of a sapper, and could not pass by. I suggest that you familiarize yourself with it. This is a story about the development of Kaboom, a clone of the legendary Minesweeper game with its own zest.

Minesweeper appeared quite a long time ago by the standards of a computer game. But it seems to me that most people remember the games that were part of earlier versions of Windows. I was never good at Minesweeper, but I played it from time to time. Some people play more seriously . And for those who want to cheer themselves up, I recommend watching Minesweeper - The Movie .

Idea

Recently, I had an idea: what if you have to play Minesweeper against a wiser computer?

Typically, the location of mines is determined at the beginning of the game (but there are a few tricks here - for example, so you can’t lose the first click). But what if the location of the mines was not determined in advance and the game could choose the location of the mines after the start of the game?

That would be pretty cruel: if you click on a square that may contain a mine, it will always contain it! Thus, you must prove in advance that the square is safe.

In the image above, in the cells marked with a dot, there are guaranteed no mines, and cells marked with an exclamation mark are guaranteed to contain one. Question marks mean uncertainty: perhaps if you open more cells, you can calculate whether a mine is hidden there or not.

On the other hand, there are situations when you have to guess:

There is a mine in one of the lower cells. But in which one, it is impossible to understand. You must choose one of them. But according to the condition that I just spoke of, this would mean certain death! I wanted the game to be brutal, but now it is obviously losing.
Therefore, I will slightly change the idea. You can guess, but only if there are no safe cells left. Thus, the game will be cruel, but fair.

In other words:

, .
, , .
, :
1. , , .
2. , , .

How to implement such a game? I could try to calculate all possible fields, but this is unrealistic: even a small 10x10 field means 2 ^ 100 possibilities. Selecting only those that contain exactly N min does not help.

Fortunately, I don’t need to worry about the whole field. We do not know anything about land mines not adjacent to tags. I am only interested in those that are on the border, the rest can be determined quite by accident.

Then I can calculate all the options for the location of mines on the border in accordance with the labels. Backtracking (backtracking) - a good technique that allows you to sort through all the combinations, but also quick to retreat as soon as we determine that a branch can not calculate.

The two possible locations of mines at the border are shown above. Combining them, we will understand which cells are guaranteed to be empty or mined.

I also need to track the total number of mines. Thus, the location really looks like “5 min at the border, 5 min outside”. This is important because otherwise I could have created too many mines at the border (or too few!)

So, I have all the options. What happens when a player decides to open a cage?

Choose a random option (one that satisfies the “cruel but fair” rules). This will determine the location of mines on the border.
Randomly scatter those remaining outside the border.
If there is a mine in the selected cell, the game is over.
Otherwise:
1. Define a new label for the identified cell
2. Reveal additional cells if it is 0
3. , ! .

For small fields this is normal. Usually there are only a few possible combinations ... wait, what is it?

Oh no!

Somehow, I managed to unlock 18 million possible mine locations. My Firefox devours 12 gigabytes of memory, and opening a cell takes half a minute. Obviously, I need a better algorithm.

Someone may notice that Minesweeper is an NP-complete game , and therefore an exponentially increasing time cannot be avoided. And in the general case, this is true - there will be positions that will take a lot of time to calculate. But for a small area this works.

I do not need to remember all the combinations. I do not even need to calculate all the combinations. All that is required is a way:

check if the cell is safe, dangerous or vague,
(, , ).

Instead of trying out the options myself, I'm going to use the SAT solver . These are tools that take a formula consisting of logical variables and look for a set of values that would make the formula true. Such an imaginary, but quite valid method for our task.

A more powerful class of software is SMT solvers that work with a wider range of values and formulas, such as first-order logic (quantifiers), arrays, integers, and so on. This will help at least define some equations for integers. But I need something that works in the browser. People managed to port some sophisticated tools like Z3Prover to the browser, but the WebAssembly version weighs17 MB , and that's too much.

I found MiniSat , a small SAT solver that was compiled for Javascript by Joel Galenson. The compiled file takes only 200 kilobytes, so I use it.

CNF Formulas

SAT solvers work with conjunctive normal formulas ( CNFs ). CNF's formula is “an AND of ORs,” for example:

(a | ~ b | ~ c) & (c | d ~ e) & f

you can convert any formula of sentence logic (variables, and, or, not, implication) to CNF, so it's kind of a universal format.

How do we use it? Suppose we have a board: If I create variables for unknown cells (clockwise: x1, x2, x3), they will have to satisfy the following equations: But how to express “the sum of the variables is 2” in CNF? I found a method that, as I later learned, is called “binomial coding” and is the simplest coding. You should consider all possible subsets of variables. For example, for you need the following formulas:

? ? 1
2 ? 1

1 + 2 + 3 = 2
2 + 3 = 1
2 + 3 = 1 ( )

x1 + x2 + x3 = 2

For each subset of 2 variables, at least one is true. This ensures that the amount is greater than 1.
(x1 | x2) & (x1 | x3) & (x2 | x3)
At least one variable is false. This ensures that the amount is less than 3.
(~ x1 | ~ x2 | ~ x3)

For x2 + x3 = 1me I need a similar set of formulas:

At least one of the variables is correct: (x2 | x3)
At least one of the variables is false (~ x2 | ~ x3).

By combining this, I get a CNF formula with 6 points. In the standard DIMACS format: All position lines end with 0, and negation is marked with a minus. If I connect it to MiniSat (try it for yourself), I get: This means that MiniSat found a solution where x1 and x2 are true and x3 are false. Here's what the board will look like: The whole program is a little more complicated: this is just one solution, there is another. Therefore, to find out if x1, x2, x3 can be true (or false), you need to make more requests. I need to ask: “Given the above formula, as well as x1, is this feasible? How about the above formula, as well as ~ x1 "?

SAT 1 2 -3

! ! 1
2 . 1

Encoding means that I need to find all possible combinations (for example, all subsets of 3) of a set of variables. However, for this equation there will only be up to 8 variables, so the formula is usually small enough so that MiniSat can quickly solve it.

Min tracking

Unfortunately, this is not a complete solution! I still need to track how many mines are left. Some combinations are impossible, because otherwise you can create more mines than allowed, and it will be impossible to win.

In fact, the opposite case is also possible: if there are too few mines, the game will end, because there will be nothing to place.

Therefore, I need to indicate in the SAT formula that “the number of mines is not less than X and not more than Y”. At first I thought I could use the trick with all the combinations. Unfortunately, it does not work too well with large numbers. If there are, say, 20 cells and 10 min, then after connecting the numbers to the binomial coefficient, we find out that the number of combinations is already 6 digits!

So I found out that there are many other ways to encode the sum of variables into the SAT formula. You need to create a schema that will combine the individual variables. See, for example, this answer on StackExchange or this one .

In the end, I realized the idea from an article entitled “Effective CNF Coding with Boolean Cardinality Constraints”, written by Olivier Baillot and Yasin Bufhad. We see a tree that recursively adds unary numbers (or sorts bits so that everyone is at the beginning):

At the end of this diagram, you will get a sorted set of “output” variables. To confirm that the sum is not less than X, check that the first X of the resulting variables are 1. To claim that the sum is not more than Y, check that the last N - Y of the resulting variables are 0.

This is much better than using all possible combinations, however, this scheme is still irrational because it generates sentences Ө (N ^ 2). When the number of open cells is about 100, the game becomes sluggish. We can optimize the game further.
Reduce Requests

While studying the issue, I noticed that I can reduce the number of queries to the solver. I wanted to determine the status of all cells (that is, to check whether they are guaranteed to be dangerous, safe or not). I did this using a simple loop. Let's say the board is described by the formula F:

Decide for F & ~ x1to check if x1 can be 0
Decide for F & x1to check if x1 can be 1
Decide for F & ~ x2 to check if x2 can be 0
Decide for F & x2to check if x2 can be 1
Etc.

What did I notice? If I get a solution for F & ~ x1, it will also contain the values of all other variables. This already answers many other questions: if the solution contains x2 = 0, I do not need to ask if x2 can be 0, because I already know this. This allows me to reduce the number of requests by about 2-5 times.

Caching

This does not solve the problem of the huge formula generated by the "counting" circuit. As I said, the number of sentences is in the order of N ^ 2. On a large board, the formula can be up to 10,000 assumptions.

Fortunately, most of the time we know the exact meaning of many cells. If the cell is guaranteed empty or guaranteed filled, the value will never change! This means that we can cache it and not include it in the SAT formula. Once we determine the state of the cell, we will no longer need to include it in the calculation again. Cells will be used as long as they are undefined.

This optimization is slightly dangerous: we no longer have a formula confirming the correctness of the entire board. If everything else works as planned, this is not a problem, but it can complicate error tracking.

Another case: playing abroad

Are you allowed to click anywhere on the map outside the border between the open and unopened area of the field?

Initially, I thought it was the same as guessing: if there are no safe cells, you can simply click anywhere on the field. But some find it strange that this guarantees the opening of an empty cage.

Therefore, I changed the game so that a click outside the border is always punished. With the exception of the start of the game, of course, because then the whole board is “outside”.

But it turns out that there is another scenario: what if all the border fields are deadly? You have no choice but to reveal something else. This situation can make the game impassable from the start. So now there is one more exception. You are allowed to play outside the borders if:

3 . .
. . .
. . .

The field is not open
The mined cells may be located on the border (clicking on the outside should be safe), or
There must be bombs in all the cells on the border (you have to click outside).

Update : The change turned out to be controversial, as the restriction is somewhat artificial. I added a switch that will allow / prohibit playing with these conditions.

It's all

You can play Kaboom here . Try turning on debugging mode: it makes the game trivial, but it shows well how it works. Github

source code . He is not very handsome. You might also be interested in a similar game from Simon Tatham, creator of PuTTY. Its version has a different twist: it is always solvable without speculation. Play wisely! What else can be useful to read on the Cloud4Y blog → How the bank “broke” → Personal privacy? No, they did not hear → The Great Theory of Snowflakes → Diagnostics of network connections on a virtual EDGE router →

CRISPR-resistant viruses build shelters to protect genomes from DNA-penetrating enzymes.

Subscribe to our Telegram channel so you won’t miss another article! We write no more than twice a week and only on business. We remind you that startups can get 1 million rubles. from Cloud4Y. Terms and conditions for those who wish - on our website: bit.ly/2sj6dPK