Solving Minesweeper on paper using SMT (integer) solver

Solving Minesweeper on paper using an SMT (integer) solver

Sunday 25 September 2022

An Article by Clive England, CEng, MBCS 

See Original and updates on https://gannett-hscp.blogspot.com  September 2022

Continuing the series of solving puzzles using an integer SMT solver we look now at the paper version of the Minesweeper puzzle. Originally Minesweeper was an active game shipped with various versions of Windows operating systems. This version is static as published in newspapers. See Minesweeper link for more information about the active game.

This popular logic puzzle is published in the i newspaper. The puzzle offers a rectangular grid with numeric clues from which the locations of hidden mines must be deduced. The initial clue numbers show the quantity of mines adjacent to the clue square. The numbers are generated by counting the hidden mines one step in any direction (kings move). No edge wraparound is allowed. No mines are located under clue squares.

Encoding

The puzzle is simply encoded into text then a script is used to generate the underlying logic of the puzzle. These logic lines are then passed to an SMT solver for analysis and resolution. Microsoft's Z3 and MathSAT solvers are used. The above puzzles are encoded as follows.

#iMine iMine_220917.txt

.0..00...2...1..

...3..3....2..0.

2....1....43.1..

3.......3.3.....

.3..2..3.3...3.1

..1.....2....3..

0....0..2..1.1..

....1.0.....1..1

.2.0...1..3.....

...0..0.0..3.22.

1.1.3....13.....

......2.....3..2

#iMine iMine_test03.txt

0...0

..1..

0...0

The puzzle logic for iMine_test03.txt is generated from the encoding as follows: 

    After some pre-amble to set the solvers into “linear integer” mode a value is declared for each of the empty “.” squares. 

    The range of that value then limited to 0 or 1. In the results of the solver a 1 indicates the presences of a mine in that square.  The numbering of the values is critical to the simplicity and generation of the logic to solve the problem.  

    Each cell in each row is numbered sequentially but there is a jump in numbers between the sequential rows. 

#iMine iMine_test03_Cell_numbers.txt

V0   V1  V2  V3  V4 

V9  V10  V11 V12 V13

V18 V19  V20 V21 V22  

The jump in value numbering is to avoid wrap around at the row edges.  For example the first cell on the second row is V9, to check the cell to left of V9 the logic generation script checks to see if V8 exists. As V8 is not defined the cell is treated as on the edge and V8 is not included in the logic definition. The same applies on the right hand edge of Row 1, where counting from cell V0,  V4 is not defined as it is a clue square and V5 is not defined as being off the edge of the board. The second row starts with V9.

    Words after a ; on the logic line are comments and are ignored.

    A value V000 is defined and set to value zero to assist with the case where the contents of an empty cell are defined by just one clue cell.

(set-logic LIA)

(set-option :produce-models true)

(set-option :produce-assignments true)

(declare-const V000 Int)

(assert (= 0 V000))

(declare-const V1 Int)           ; Row 1

(assert (or (= 1 V1) (= 0 V1)))

(declare-const V2 Int)

(assert (or (= 1 V2) (= 0 V2)))

(declare-const V3 Int)

(assert (or (= 1 V3) (= 0 V3)))

(declare-const V9 Int)           ; Row 2

(assert (or (= 1 V9) (= 0 V9)))

(declare-const V10 Int)

....

(declare-const V21 Int)

(assert (or (= 1 V21) (= 0 V21)))

The main logic of the puzzle is generated, one line for each of the numeric clue squares.  Each of the potential mine squares has to be 0 or 1 with the total number of 1s in the surrounding 8 squares being the same as the provided clue. Mines cannot be under clue squares. 

(assert (or (= 1 V21) (= 0 V21)))

(assert ( = 0 ( + V000 V1 V9 V10 )))       ; sqr=0 

(assert ( = 0 ( + V000 V3 V12 V13 )))       ; sqr=4 

(assert ( = 1 ( + V000 V1 V2 V3 V10 V12 V19 V20 V21 )))       ; sqr=11 

(assert ( = 0 ( + V000 V9 V10 V19 )))       ; sqr=18 

(assert ( = 0 ( + V000 V12 V13 V21 )))       ; sqr=22 

After testing it was found that some boards generate logic such as 

    (assert ( = 1 ( + V11 ))) ; sqr=10

giving an SMT error

    (error "ERROR: + takes at least 2 arguments (1 given) (line: 256)")

The was fixed by this defining V000 being value 0 and then generating the logic line

    (assert ( = 1 ( + V000 V11 ))) ; sqr=10

Finally, after triggering the satisfiability of the logic, the values of the possible mine holding squares are output. 

(check-sat)

(get-value ( V1 V2 V3 V9 V10 V12 V13 V19 V20 V21  ))

(exit)

The above logic is provided to the SMT logic solver Mathsat5 ( or Microsoft’s 3 ) and the results are obtained.

sat

( (V1 0)

  (V2 1)

  (V3 0)

  (V9 0)

  (V10 0)

  (V12 0)

  (V13 0)

  (V19 0)

  (V20 0)

  (V21 0) )

The results are read, alongside re-reading the puzzle file, to generate answer display table in html. The Red “<->” squares indicate the placement of a hidden mine. Green “.” squares are empty, clue squares show the clue value.

Result validation

Using the results from the solver each of the clue number squares are checked to see if the final solution is validated.

To check the validation one of the provided answer values is changed and .

$ ./iMine_smt.pl < iMine_220917.txt | ~/CodeProjects/solver_m5 | sed 's/(V43 0)/(V43 1)/'|  

  ./iMine_smt.pl -f iMine_220917.txt  > iMine_220917.html

Two dreamboards

In active Minesweeper a dreamboard is a very easy intermediate game that can be solved in record times. Full exploration here  Two are solved here in about   real 0m0.048s each.

Paper Versus active game

The dream boards, taken from the active game, are showing up the gap between the active game and the paper version of the game. In the active game there are situations where you just have to hold breath and guess because not all the clues are exposed at the beginning. In the paper game all the mines / no mines should be deductible from the provided clues. The solver has suggested placed mines in the open ground where there is no evidence from the clues that there are or are not mines. Because the clues in the paper game are incomplete the results are somewhat indeterminate. 

In this section half way down on the right hand side of dreamboard_001

.	.	.
.	.	.
.	1	1
.	2	.
.	3	.
.	2	.
.	1	1
.	.	.

There are two possible valid answers from the clues provided, the one given by the solver suitable for the paper game

and the one shown in the active game solution.

In the active game the has the "No mines can have naked edges" rule that does not apply in the paper version of the game. This causes the anomaly. A few carefully placed 0s would guide the solver away from the large open areas. A 0 diagonally near the 3 in the section above would resolve the dilemma in this case. 

Cartoons

Some Minesweeper cartoons here.

References

Programming Z3 Sudoku section from Section 8.1 page 139

Building a Sudoku Solver with SAT,  

A SAT-based Sudoku Solver,  

Sudoku as a SAT Problem, 

Optimized CNF Encoding for Sudoku Puzzles 

Mathsat5 solver

Usage for the Minesweeper to SMT generation utility

Usage: Minesweeper {options} < puzzle.txt  or

    Minesweeper {options} -f puzzle.txt < SolverOutput

    -v N :Be verbose to level N ( use v=1 for detailed output )

    -f puzzle.txt :puzzle file needed when reading Solver output use STDIN otherwise

    

    Programs reads STDIN looking for either puzzleFile format lines or Solver output lines

        If the input is in puzzleFile format the program will generate solver input lines.

        If the input is in Solver output lines format the program will expect a -f puzzleFile paremeter.

            Using both these input streams program will then generate display .html output.

Game Rules

        The layout of a minefield is described using a rectangular grid with integers and gaps.

        Each number indicates the proximity of mines on directly adjcent squares (8 directions)

        Mines cannot be on numbered squares and there is no board wraparound.

Each Minesweeper puzzle Input as follows can be any size rectangle

        

        #iMine iMine_220917.txt

        .0..00...2...1..

        ...3..3....2..0.

        2....1....43.1..

        3.......3.3.....

        .3..2..3.3...3.1

        ..1.....2....3..

        0....0..2..1.1..

        ....1.0.....1..1

        .2.0...1..3.....

        ...0..0.0..3.22.

        1.1.3....13.....

        ......2.....3..2

        

        or this minimal test

        

        #iMine iMine_test03.txt

        0...0

        ..1..

        0...0

to generate an SMT2 input file.

OR Process results from solver in the following format

    sat

    ( (V0 9)

    (V1 7)

    (V2 5)

    (V3 3)

    ....

to generate an html table as output. 

The Solver results are read,

        alongside re-reading the puzzle file, to generate answer

        display table in html. The Red “<->” squares indicate the

        placement of a hidden mine. Green “.” squares are empty,

        clue squares show the clue value.

The results are validated by checking each of the clue numbers

        has the correct numbers of mines in the surrounding squares.

VALIDATION FAIL or VALIDATION PASS is provided.

        

SMT Solvers, introduction and links (Start here with the readme)

Satisfiability modulo theories library, is the a grand title given to what we will refer to as SMT – Lib or even just SMT. This blog and its associated articles are the result of trying to find some software that would both complete every possible known Sudoku and provide a way forward for a problem solving project that was bogged down. 

SMT has quite a high barrier to entry, the descriptions of how they work and what they can do are very mathematically orientated, using symbols and characters that are unfamiliar to most computer programming folks. However, with a little perseverance, trial and error, they can be a great stepping stone toward solving a multitude of different problems. 

Starting out with solving Sudoku in mind. The initial step was understanding how to describe the rules of Sudoku in a way that can be presented to a general purpose, SMT solver. Unlike other programming approaches, the required effort is around describing the rules and conditions of the problem whilst completely ignoring how to progress those rules to reach an answer. The solver takes on all the effort of reconciling the constraints of the particular puzzle, giving a viable answer or rejecting the puzzle as unsatisfiable. 

Gone is the complexity of implementing the many solving rules for Sudoku replaced by a simple text manipulation script that reads the input puzzle, generates a SMT language file, passes it to the solver then reads the solver results. This solution pipeline can be applied to many different puzzle types ( but not crosswords) with just minor adjustments to the scripts.

The stages of the puzzle solving pipeline are are :

• Image of Puzzle,
• Text representation of puzzle,
• Script to convert from text to SMT language,
• Solver,
• Script to convert results to a display.

A detailed writeup on Sudoku and some of its variants can be found here but the short description is as follows :

• Tell solver what type problem this is and that answer values will be required
• Declare 81 integers each of which can only have values between 1 and 9.
• Declare that each row, column and sub-square must have unique values,
• Set the known clue numbers,
• Ask for the answers

By describing the problem in this exact way the solver will find an answer. For sudoku puzzles of different shapes and answer values, the number of variables and their range can be simply adjusted in the conversion script.

The solver used is not artificial intelligence. They are entirely deterministic and driven purely by the input statements provided to them. By defining the problem in strict logical terms, that logic can be manipulated in order to find the answers. No guesswork or training is required by the solver. Every answer is logically deducted from the provided input statements. 

Following on from the success of solving any type and shape of Sudoku, other puzzles were tackled using a similar techniques. The wrinkle being some of the problems require careful manipulation in order to create the required SMT language. The conversion of results into a displayable page image was mostly taken care of using generated HTML text displayed in a browser. 

SMT solvers have traditionally been used in the rarefied areas of theorem proofing and program integrity, checking. There use here whilst less formal provides some insight into how deconstructing a problem into its core aspects, and then concentrating just on those features can provide a useful introduction to 1st order logic and getting the job done quickly.

Solving Kurosu using Perl and C

 Kurosu is a combinatorial bit seeing puzzle from the DM - but is not so hard.

** Update See how this puzzle is solved using an SMT solver. ( this is an old post )

The puzzle is just a 36 bit solver.

Each Row/Column must have 3 * 0 and 3 * X

In line positioning - No more than 2 lots of 00 or XX allowed. This could be better worded as no 3  O or X together in a row or column.

First glance:

   Using 1 as x and 0 as O.

   There are 36 cells each of which can have 2 different values.

   Each line (row or column) must have 3*1s and 3*0s
   No line with "111" or "000" is allowed 

   Number of patterns of 6 bits that have 3*0 and 3*1 = 20 ( some will have 3 in a row and need to be excluded )

    

Because of the line pattern rules:

    Total number of line patterns will be substantially less than 2^6 aka 64

    Total number of puzzle patterns will be substantially less than 2^36 aka  68,719,476,736

After research :

    Total number of actual line patterns that follow the rules above is 14.

    As each line pattern can be used more than once in the puzzle the ..

    Total number of possible puzzle patterns that follow the line rules above is = 14^6 = 7,529,536

    Actual total number of valid puzzle patterns that follow the rules above is just 11,222

By comparison all the puzzle layouts is less than the number of possible layouts for a single Sudoku line (362,879).

Sample puzzle : 

Looking in detail at the line patterns that match the rules:

#Kurosu v1.0 June 2018 estimate 11222

#Pat Count = 14

[0] 11 = 0x0b = 001011

[1] 13 = 0x0d = 010011

[2] 19 = 0x13 = 001101

[3] 21 = 0x15 = 010101

[4] 22 = 0x16 = 100101

[5] 25 = 0x19 = 011001

[6] 26 = 0x1a = 101001

[7] 37 = 0x25 = 010110

[8] 38 = 0x26 = 100110

[9] 41 = 0x29 = 011010

[10] 42 = 0x2a = 101010

[11] 44 = 0x2c = 110010

[12] 50 = 0x32 = 101100

[13] 52 = 0x34 = 110100

Board patterns that match the rules are obtained by permuting all the line patterns and testing for compilance :

Pass Permutation# result# { line numbers,... } puzzle_result_pattern.

# board lines, tableMax = 7529535

Pass 35867 1 { 13 13 0 13 0 0 } 110100110100001011110100001011001011

Pass 36049 2 { 13 12 1 13 0 0 } 110100101100010011110100001011001011

Pass 36231 3 { 13 11 2 13 0 0 } 110100110010001101110100001011001011

Pass 36413 4 { 13 10 3 13 0 0 } 110100101010010101110100001011001011

Pass 36595 5 { 13 9 4 13 0 0 } 110100011010100101110100001011001011

Pass 36777 6 { 13 8 5 13 0 0 } 110100100110011001110100001011001011

Pass 36959 7 { 13 7 6 13 0 0 } 110100010110101001110100001011001011

……snip 

Pass 7492758 11217 { 0 5 8 0 13 13 } 001011011001100110001011110100110100

Pass 7492940 11218 { 0 4 9 0 13 13 } 001011100101011010001011110100110100

Pass 7493122 11219 { 0 3 10 0 13 13 } 001011010101101010001011110100110100

Pass 7493304 11220 { 0 2 11 0 13 13 } 001011001101110010001011110100110100

Pass 7493486 11221 { 0 1 12 0 13 13 } 001011010011101100001011110100110100

Pass 7493668 11222 { 0 0 13 0 13 13 } 001011001011110100001011110100110100

Solving

Given that a line can be considered as horizontal or vertical...

Solving Rule 1: Line can be trivially completed when first showing either 3*0 or 3*1.

Solving Rule 2: A vertical or horizontal line solved contributes to all other lines that cross it.

Solving Rule 3: Only one solution should found in the board patterns.

Can be simply solved using pattern grep after all 11,222 possible board layouts are calculated.

Using a sample puzzle file

$ cat ku_dm_01062018.txt

#Kurosu6 DM 01 June 2018

...0.1

0...0.

1.1.1.

..0...

.1.0.1

0....0

Solving by shell and Perl - join up the board lines and search the possible board solutions found within the pre-calculated Tables file that holds all the possible board layout results.

1> $ for i in ku_dm_* ; 

2>   do  echo $i ; 

3>   cat $i | perl -ane '{ next if (/^#/); $b.=$_ };  

4>           END { $b=~s/\n//g; print "Board>$b\n";

5>           system "grep \" $b\$\" < ./TablesForKurosu.txt"; };'; 

6>  done

giving

ku_dm_01062018.txt

Board>...0.10...0.1.1.1...0....1.0.10....0

Pass 3980808 5844 { 6 3 10 8 5 7 } 101001010101101010100110011001010110

displayed as 

101001

010101

101010

100110

011001

010110

Solving explanation line by line

1> Run script in a loop for all the files named ku_dm_...........
2> Print the filename ( $i ) for this loop instance
3> Send the file contents to a Perl script that eats the input line by line but skips lines starting with a #. Other lines are assembled into $b.
4> At the END of the input file remove by substitution all the line ending markers. Print the board as a single line starting Board.
5> Call the unix system command grep (global regular expression print) to print all lines in the file TablesForKurosu.txt that contain a pattern match for the input board. The input board lines have . as the unknown values which is the wildcard search character in grep.

We see that this works by having a sample of input puzzle files all of which find only one and only one of the pre-calculated board layouts.

Results

ku_dm_01062018.txt

Board>...0.10...0.1.1.1...0....1.0.10....0

Pass 3980808 5844 { 6 3 10 8 5 7 } 101001010101101010100110011001010110

ku_dm_04062018.txt

Board>..1.1..0.1.....1.0...0.0..1......11.

Pass 4022564 6097 { 0 4 13 9 6 7 } 001011100101110100011010101001010110

ku_dm_05062018.txt

Board>.1...11...1..011....1.0..1.1..1..01.

Pass 5664165 8663 { 3 11 2 6 7 10 } 010101110010001101101001010110101010

ku_dm_06062018.txt

Board>......0..01.....0.1.....1....1..1.11

Pass 184379 167 { 13 9 2 11 4 0 } 110100011010001101110010100101001011

ku_dm_07062108.txt

Board>...0.0.1....0.1...0..1......1..110..

Pass 3004872 4390 { 10 13 0 3 8 5 } 101010110100001011010101100110011001

ku_dm_12062018.txt

Board>..1.....1.1.........00...1...1......

Pass 4525768 6852 { 2 9 4 11 5 8 } 001101011010100101110010011001100110

ku_dm_13062018.txt

Board>..1.0..11....1..0......10..........1

Pass 2422888 3501 { 6 9 13 0 7 4 } 101001011010110100001011010110100101

ku_dm_14062018.txt

Board>00..0..........0...1...10....1.01.0.

Pass 6502652 9800 { 2 11 10 3 1 12 } 001101110010101010010101010011101100

ku_dm_16062018.txt

Board>11..1......0...1...1.....0.1.0..0.0.

Pass 2077751 3189 { 11 10 2 1 12 3 } 110010101010001101010011101100010101

Solving using c++

1: Read the input puzzle file into an array of 6 strings.

2: For each string match against all 14 of the possible line patterns retaining a list of those that match.

3: Multiply the lengths of the lists to get the total number of pattern perms that are to be tested against the rules and input puzzle

4: Generate from the lists of sub-string patterns possible board answer layouts. 

5: Test against the board rules and input pattern until solution is found. 

Interesting coding point

Having generated a possible solution layout using horizontal sub-strings the solution needs to be transformed to enable easier checking of the solution. Equivalent to rotating the board by 90 degrees.

// l 001101 001011 001011 010011 001011 001101  Transformation from rows to cols gives

// v 000000 000100 111011 100001 011110 111111  

//   ab  becomes ax

//   xy          by

Transformation of a bit matrix is described in the seminal book Hacker's Delight by Henry S. Warren who's code is available here but only works on 32 bit machines apparently. However I just used a simpler substr char by char method.

for (j=0; j<=5; j++) { // transpose board to be able to read down the colls

        vboard = vboard + lboard.substr(j+0,1)  + lboard.substr(j+6,1) + 

                          lboard.substr(j+12,1) + lboard.substr(j+18,1) +

                          lboard.substr(j+24,1)+ lboard.substr(j+30,1);

}