## 7-Mar-2017: Cracking Minesweeper with SAT solver

(The following text has been moved to the article at https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.)

(Previously: https://yurichev.com/blog/minesweeper/.)

SAT solvers are very different in that sense that they are at low-level, and can take only CNF expressions on input. I wrote a very short intro into SAT, right at the beginning of the following article: https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf, which you can skim quickly before proceeding to the rest of this blog post.

### Simple population count function

First of all, somehow we need to count neighbour bombs. The counting function is very similar to population count function.

We can try to make CNF expression in Wolfram Mathematica. This will be a function, returning True if any of 2 bits of 8 inputs bits are True and others are False. First, we make truth table of such function:

In[]:= tbl2 =
Table[PadLeft[IntegerDigits[i, 2], 8] ->
If[Equal[DigitCount[i, 2][[1]], 2], 1, 0], {i, 0, 255}]

Out[]= {{0, 0, 0, 0, 0, 0, 0, 0} -> 0, {0, 0, 0, 0, 0, 0, 0, 1} -> 0,
{0, 0, 0, 0, 0, 0, 1, 0} -> 0, {0, 0, 0, 0, 0, 0, 1, 1} -> 1,
{0, 0, 0, 0, 0, 1, 0, 0} -> 0, {0, 0, 0, 0, 0, 1, 0, 1} -> 1,
{0, 0, 0, 0, 0, 1, 1, 0} -> 1, {0, 0, 0, 0, 0, 1, 1, 1} -> 0,
{0, 0, 0, 0, 1, 0, 0, 0} -> 0, {0, 0, 0, 0, 1, 0, 0, 1} -> 1,
{0, 0, 0, 0, 1, 0, 1, 0} -> 1, {0, 0, 0, 0, 1, 0, 1, 1} -> 0,
...
{1, 1, 1, 1, 1, 0, 1, 0} -> 0, {1, 1, 1, 1, 1, 0, 1, 1} -> 0,
{1, 1, 1, 1, 1, 1, 0, 0} -> 0, {1, 1, 1, 1, 1, 1, 0, 1} -> 0,
{1, 1, 1, 1, 1, 1, 1, 0} -> 0, {1, 1, 1, 1, 1, 1, 1, 1} -> 0}


Now we can make CNF expression using this truth table:

In[]:= BooleanConvert[
BooleanFunction[tbl2, {a, b, c, d, e, f, g, h}], "CNF"]

Out[]= (! a || ! b || ! c) && (! a || ! b || ! d) && (! a || !
b || ! e) && (! a || ! b || ! f) && (! a || ! b || ! g) && (!
a || ! b || ! h) && (! a || ! c || ! d) && (! a || ! c || !
e) && (! a || ! c || ! f) && (! a || ! c || ! g) && (! a || !
c || ! h) && (! a || ! d || ! e) && (! a || ! d || ! f) && (!
a || ! d || ! g) && (! a || ! d || ! h) && (! a || ! e || !
f) && (! a || ! e || ! g) && (! a || ! e || ! h) && (! a || !
f || ! g) && (! a || ! f || ! h) && (! a || ! g || ! h) && (a ||
b || c || d || e || f || g) && (a || b || c || d || e || f ||
h) && (a || b || c || d || e || g || h) && (a || b || c || d || f ||
g || h) && (a || b || c || e || f || g || h) && (a || b || d ||
e || f || g || h) && (a || c || d || e || f || g ||
h) && (! b || ! c || ! d) && (! b || ! c || ! e) && (! b || !
c || ! f) && (! b || ! c || ! g) && (! b || ! c || ! h) && (!
b || ! d || ! e) && (! b || ! d || ! f) && (! b || ! d || !
g) && (! b || ! d || ! h) && (! b || ! e || ! f) && (! b || !
e || ! g) && (! b || ! e || ! h) && (! b || ! f || ! g) && (!
b || ! f || ! h) && (! b || ! g || ! h) && (b || c || d || e ||
f || g ||
h) && (! c || ! d || ! e) && (! c || ! d || ! f) && (! c || !
d || ! g) && (! c || ! d || ! h) && (! c || ! e || ! f) && (!
c || ! e || ! g) && (! c || ! e || ! h) && (! c || ! f || !
g) && (! c || ! f || ! h) && (! c || ! g || ! h) && (! d || !
e || ! f) && (! d || ! e || ! g) && (! d || ! e || ! h) && (!
d || ! f || ! g) && (! d || ! f || ! h) && (! d || ! g || !
h) && (! e || ! f || ! g) && (! e || ! f || ! h) && (! e || !
g || ! h) && (! f || ! g || ! h)


The syntax is similar to C/C++. Let's check it.

I wrote a Python function to convert Mathematica's output into CNF file which can be feeded to SAT solver:

#!/usr/bin/python

import subprocess

def mathematica_to_CNF (s, a):
s=s.replace("a", a[0]).replace("b", a[1]).replace("c", a[2]).replace("d", a[3])
s=s.replace("e", a[4]).replace("f", a[5]).replace("g", a[6]).replace("h", a[7])
s=s.replace("!", "-").replace("||", " ").replace("(", "").replace(")", "")
s=s.split ("&&")
return s

def POPCNT2 (a):
s="(!a||!b||!c)&&(!a||!b||!d)&&(!a||!b||!e)&&(!a||!b||!f)&&(!a||!b||!g)&&(!a||!b||!h)&&(!a||!c||!d)&&" \
"(!a||!c||!e)&&(!a||!c||!f)&&(!a||!c||!g)&&(!a||!c||!h)&&(!a||!d||!e)&&(!a||!d||!f)&&(!a||!d||!g)&&" \
"(!a||!d||!h)&&(!a||!e||!f)&&(!a||!e||!g)&&(!a||!e||!h)&&(!a||!f||!g)&&(!a||!f||!h)&&(!a||!g||!h)&&" \
"(a||b||c||d||e||f||g)&&(a||b||c||d||e||f||h)&&(a||b||c||d||e||g||h)&&(a||b||c||d||f||g||h)&&" \
"(a||b||c||e||f||g||h)&&(a||b||d||e||f||g||h)&&(a||c||d||e||f||g||h)&&(!b||!c||!d)&&(!b||!c||!e)&&" \
"(!b||!c||!f)&&(!b||!c||!g)&&(!b||!c||!h)&&(!b||!d||!e)&&(!b||!d||!f)&&(!b||!d||!g)&&(!b||!d||!h)&&" \
"(!b||!e||!f)&&(!b||!e||!g)&&(!b||!e||!h)&&(!b||!f||!g)&&(!b||!f||!h)&&(!b||!g||!h)&&(b||c||d||e||f||g||h)&&" \
"(!c||!d||!e)&&(!c||!d||!f)&&(!c||!d||!g)&&(!c||!d||!h)&&(!c||!e||!f)&&(!c||!e||!g)&&(!c||!e||!h)&&" \
"(!c||!f||!g)&&(!c||!f||!h)&&(!c||!g||!h)&&(!d||!e||!f)&&(!d||!e||!g)&&(!d||!e||!h)&&(!d||!f||!g)&&" \
"(!d||!f||!h)&&(!d||!g||!h)&&(!e||!f||!g)&&(!e||!f||!h)&&(!e||!g||!h)&&(!f||!g||!h)"
return mathematica_to_CNF(s, a)

clauses=POPCNT2(["1","2","3","4","5","6","7","8"])

f=open("tmp.cnf", "w")
f.write ("p cnf 8 "+str(len(clauses))+"\n")
for c in clauses:
f.write(c+" 0\n")
f.close()



It replaces a/b/c/... variables to the variable names passed (1/2/3...), reworks syntax, etc. Here is a result:

p cnf 8 64
-1 -2 -3 0
-1 -2 -4 0
-1 -2 -5 0
-1 -2 -6 0
-1 -2 -7 0
-1 -2 -8 0
-1 -3 -4 0
-1 -3 -5 0
-1 -3 -6 0
-1 -3 -7 0
-1 -3 -8 0
-1 -4 -5 0
-1 -4 -6 0
-1 -4 -7 0
-1 -4 -8 0
-1 -5 -6 0
-1 -5 -7 0
-1 -5 -8 0
-1 -6 -7 0
-1 -6 -8 0
-1 -7 -8 0
1 2 3 4 5 6 7 0
1 2 3 4 5 6 8 0
1 2 3 4 5 7 8 0
1 2 3 4 6 7 8 0
1 2 3 5 6 7 8 0
1 2 4 5 6 7 8 0
1 3 4 5 6 7 8 0
-2 -3 -4 0
-2 -3 -5 0
-2 -3 -6 0
-2 -3 -7 0
-2 -3 -8 0
-2 -4 -5 0
-2 -4 -6 0
-2 -4 -7 0
-2 -4 -8 0
-2 -5 -6 0
-2 -5 -7 0
-2 -5 -8 0
-2 -6 -7 0
-2 -6 -8 0
-2 -7 -8 0
2 3 4 5 6 7 8 0
-3 -4 -5 0
-3 -4 -6 0
-3 -4 -7 0
-3 -4 -8 0
-3 -5 -6 0
-3 -5 -7 0
-3 -5 -8 0
-3 -6 -7 0
-3 -6 -8 0
-3 -7 -8 0
-4 -5 -6 0
-4 -5 -7 0
-4 -5 -8 0
-4 -6 -7 0
-4 -6 -8 0
-4 -7 -8 0
-5 -6 -7 0
-5 -6 -8 0
-5 -7 -8 0
-6 -7 -8 0



I can run it:

% minisat -verb=0 tst1.cnf results.txt
WARNING: for repeatability, setting FPU to use double precision
SATISFIABLE

% cat results.txt
SAT
1 -2 -3 -4 -5 -6 -7 8 0


The variable name in results lacking minus sign is "True". Variable name with minus sign is "False". We see there are just two variables are "True": 1 and 8. This is indeed correct: MiniSat solver found a condition, for which our function returns "True". Zero at the end is just a terminal symbol which means nothing.

We can ask MiniSat for another solution, by adding current solution to the input CNF file, but with all variables negated:

...
-5 -6 -8 0
-5 -7 -8 0
-6 -7 -8 0
-1 2 3 4 5 6 7 -8 0


In plain English language, this means "give me ANY solution which can satisfy all clauses, but also not equal to the last clause we've just added".

MiniSat, indeed, found another solution, again, with only 2 variables equal to "True":

% minisat -verb=0 tst2.cnf results.txt
WARNING: for repeatability, setting FPU to use double precision
SATISFIABLE

% cat results.txt
SAT
1 2 -3 -4 -5 -6 -7 -8 0


By the way, population count function for 8 neighbours in CNF form is simplest:

a&&b&&c&&d&&e&&f&&g&&h


Indeed: it's true if all 8 input bits are "True".

The function for 0 neighbours is also simple:

!a&&!b&&!c&&!d&&!e&&!f&&!g&&!h


It means, it will return "True", if all input variables are "False".

By the way, function for POPCNT1 is also simple:

(!a||!b)&&(!a||!c)&&(!a||!d)&&(!a||!e)&&(!a||!f)&&(!a||!g)&&(!a||!h)&&(a||b||c||d||e||f||g||h)&&
(!b||!c)&&(!b||!d)&&(!b||!e)&&(!b||!f)&&(!b||!g)&&(!b||!h)&&(!c||!d)&&(!c||!e)&&(!c||!f)&&(!c||!g)&&
(!c||!h)&&(!d||!e)&&(!d||!f)&&(!d||!g)&&(!d||!h)&&(!e||!f)&&(!e||!g)&&(!e||!h)&&(!f||!g)&&(!f||!h)&&(!g||!h)


It just enumerates all possible pairs of 8 variables (a/b, a/c, a/d, etc) and says: no two bits must be present simultaneously in each possible pair. And there is another clause: "(a||b||c||d||e||f||g||h)", which says: at least one bit must be present among 8 variables.

And yes, you can ask Mathematica for finding CNF expressions for any other truth table.

### Minesweeper

Now we can use Mathematica to get all population count functions for 0..8 neighbours.

For 9*9 Minesweeper grid including invisible border, there will be 11*11=121 variables, mapped to Minesweeper grid like this:

 1    2   3   4   5   6   7   8   9  10  11
12   13  14  15  16  17  18  19  20  21  22
23   24  25  26  27  28  29  30  31  32  33
34   35  36  37  38  39  40  41  42  43  44

...

100 101 102 103 104 105 106 107 108 109 110
111 112 113 114 115 116 117 118 119 120 121


Then we write a Python script which stacks all population count functions: each function for each known number of neighbours (digit on Minesweeper field). Each POPCNTx() function takes list of variable numbers and outputs list of clauses to be added to the final CNF file.

As of empty cells, we also add them as clauses, but with minus sign, which means, the variable must be False. Whenever we try to place bomb, we add its variable as clause without minus sign, this means the variable must be True.

Then we execute external minisat process. The only thing we need from it is exit code. If an input CNF is UNSAT, it returns 20:

#!/usr/bin/python

import subprocess

WIDTH=9
HEIGHT=9
VARS_TOTAL=(WIDTH+2)*(HEIGHT+2)

known=[
"01?10001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"????1001?",
"????3101?",
"?????211?",
"?????????"]

def mathematica_to_CNF (s, a):
s=s.replace("a", a[0]).replace("b", a[1]).replace("c", a[2]).replace("d", a[3])
s=s.replace("e", a[4]).replace("f", a[5]).replace("g", a[6]).replace("h", a[7])
s=s.replace("!", "-").replace("||", " ").replace("(", "").replace(")", "")
s=s.split ("&&")
return s

def POPCNT0 (a):
s="!a&&!b&&!c&&!d&&!e&&!f&&!g&&!h"
return mathematica_to_CNF(s, a)

def POPCNT1 (a):
s="(!a||!b)&&(!a||!c)&&(!a||!d)&&(!a||!e)&&(!a||!f)&&(!a||!g)&&(!a||!h)&&(a||b||c||d||e||f||g||h)&&" \
"(!b||!c)&&(!b||!d)&&(!b||!e)&&(!b||!f)&&(!b||!g)&&(!b||!h)&&(!c||!d)&&(!c||!e)&&(!c||!f)&&(!c||!g)&&" \
"(!c||!h)&&(!d||!e)&&(!d||!f)&&(!d||!g)&&(!d||!h)&&(!e||!f)&&(!e||!g)&&(!e||!h)&&(!f||!g)&&(!f||!h)&&(!g||!h)"
return mathematica_to_CNF(s, a)

def POPCNT2 (a):
s="(!a||!b||!c)&&(!a||!b||!d)&&(!a||!b||!e)&&(!a||!b||!f)&&(!a||!b||!g)&&(!a||!b||!h)&&(!a||!c||!d)&&" \
"(!a||!c||!e)&&(!a||!c||!f)&&(!a||!c||!g)&&(!a||!c||!h)&&(!a||!d||!e)&&(!a||!d||!f)&&(!a||!d||!g)&&" \
"(!a||!d||!h)&&(!a||!e||!f)&&(!a||!e||!g)&&(!a||!e||!h)&&(!a||!f||!g)&&(!a||!f||!h)&&(!a||!g||!h)&&" \
"(a||b||c||d||e||f||g)&&(a||b||c||d||e||f||h)&&(a||b||c||d||e||g||h)&&(a||b||c||d||f||g||h)&&" \
"(a||b||c||e||f||g||h)&&(a||b||d||e||f||g||h)&&(a||c||d||e||f||g||h)&&(!b||!c||!d)&&(!b||!c||!e)&&" \
"(!b||!c||!f)&&(!b||!c||!g)&&(!b||!c||!h)&&(!b||!d||!e)&&(!b||!d||!f)&&(!b||!d||!g)&&(!b||!d||!h)&&" \
"(!b||!e||!f)&&(!b||!e||!g)&&(!b||!e||!h)&&(!b||!f||!g)&&(!b||!f||!h)&&(!b||!g||!h)&&(b||c||d||e||f||g||h)&&" \
"(!c||!d||!e)&&(!c||!d||!f)&&(!c||!d||!g)&&(!c||!d||!h)&&(!c||!e||!f)&&(!c||!e||!g)&&(!c||!e||!h)&&" \
"(!c||!f||!g)&&(!c||!f||!h)&&(!c||!g||!h)&&(!d||!e||!f)&&(!d||!e||!g)&&(!d||!e||!h)&&(!d||!f||!g)&&" \
"(!d||!f||!h)&&(!d||!g||!h)&&(!e||!f||!g)&&(!e||!f||!h)&&(!e||!g||!h)&&(!f||!g||!h)"
return mathematica_to_CNF(s, a)

def POPCNT3 (a):
s="(!a||!b||!c||!d)&&(!a||!b||!c||!e)&&(!a||!b||!c||!f)&&(!a||!b||!c||!g)&&(!a||!b||!c||!h)&&" \
"(!a||!b||!d||!e)&&(!a||!b||!d||!f)&&(!a||!b||!d||!g)&&(!a||!b||!d||!h)&&(!a||!b||!e||!f)&&" \
"(!a||!b||!e||!g)&&(!a||!b||!e||!h)&&(!a||!b||!f||!g)&&(!a||!b||!f||!h)&&(!a||!b||!g||!h)&&" \
"(!a||!c||!d||!e)&&(!a||!c||!d||!f)&&(!a||!c||!d||!g)&&(!a||!c||!d||!h)&&(!a||!c||!e||!f)&&" \
"(!a||!c||!e||!g)&&(!a||!c||!e||!h)&&(!a||!c||!f||!g)&&(!a||!c||!f||!h)&&(!a||!c||!g||!h)&&" \
"(!a||!d||!e||!f)&&(!a||!d||!e||!g)&&(!a||!d||!e||!h)&&(!a||!d||!f||!g)&&(!a||!d||!f||!h)&&" \
"(!a||!d||!g||!h)&&(!a||!e||!f||!g)&&(!a||!e||!f||!h)&&(!a||!e||!g||!h)&&(!a||!f||!g||!h)&&" \
"(a||b||c||d||e||f)&&(a||b||c||d||e||g)&&(a||b||c||d||e||h)&&(a||b||c||d||f||g)&&(a||b||c||d||f||h)&&" \
"(a||b||c||d||g||h)&&(a||b||c||e||f||g)&&(a||b||c||e||f||h)&&(a||b||c||e||g||h)&&(a||b||c||f||g||h)&&" \
"(a||b||d||e||f||g)&&(a||b||d||e||f||h)&&(a||b||d||e||g||h)&&(a||b||d||f||g||h)&&(a||b||e||f||g||h)&&" \
"(a||c||d||e||f||g)&&(a||c||d||e||f||h)&&(a||c||d||e||g||h)&&(a||c||d||f||g||h)&&(a||c||e||f||g||h)&&" \
"(a||d||e||f||g||h)&&(!b||!c||!d||!e)&&(!b||!c||!d||!f)&&(!b||!c||!d||!g)&&(!b||!c||!d||!h)&&" \
"(!b||!c||!e||!f)&&(!b||!c||!e||!g)&&(!b||!c||!e||!h)&&(!b||!c||!f||!g)&&(!b||!c||!f||!h)&&" \
"(!b||!c||!g||!h)&&(!b||!d||!e||!f)&&(!b||!d||!e||!g)&&(!b||!d||!e||!h)&&(!b||!d||!f||!g)&&" \
"(!b||!d||!f||!h)&&(!b||!d||!g||!h)&&(!b||!e||!f||!g)&&(!b||!e||!f||!h)&&(!b||!e||!g||!h)&&" \
"(!b||!f||!g||!h)&&(b||c||d||e||f||g)&&(b||c||d||e||f||h)&&(b||c||d||e||g||h)&&(b||c||d||f||g||h)&&" \
"(b||c||e||f||g||h)&&(b||d||e||f||g||h)&&(!c||!d||!e||!f)&&(!c||!d||!e||!g)&&(!c||!d||!e||!h)&&" \
"(!c||!d||!f||!g)&&(!c||!d||!f||!h)&&(!c||!d||!g||!h)&&(!c||!e||!f||!g)&&(!c||!e||!f||!h)&&" \
"(!c||!e||!g||!h)&&(!c||!f||!g||!h)&&(c||d||e||f||g||h)&&(!d||!e||!f||!g)&&(!d||!e||!f||!h)&&" \
"(!d||!e||!g||!h)&&(!d||!f||!g||!h)&&(!e||!f||!g||!h)"
return mathematica_to_CNF(s, a)

def POPCNT4 (a):
s="(!a||!b||!c||!d||!e)&&(!a||!b||!c||!d||!f)&&(!a||!b||!c||!d||!g)&&(!a||!b||!c||!d||!h)&&" \
"(!a||!b||!c||!e||!f)&&(!a||!b||!c||!e||!g)&&(!a||!b||!c||!e||!h)&&(!a||!b||!c||!f||!g)&&" \
"(!a||!b||!c||!f||!h)&&(!a||!b||!c||!g||!h)&&(!a||!b||!d||!e||!f)&&(!a||!b||!d||!e||!g)&&" \
"(!a||!b||!d||!e||!h)&&(!a||!b||!d||!f||!g)&&(!a||!b||!d||!f||!h)&&(!a||!b||!d||!g||!h)&&" \
"(!a||!b||!e||!f||!g)&&(!a||!b||!e||!f||!h)&&(!a||!b||!e||!g||!h)&&(!a||!b||!f||!g||!h)&&" \
"(!a||!c||!d||!e||!f)&&(!a||!c||!d||!e||!g)&&(!a||!c||!d||!e||!h)&&(!a||!c||!d||!f||!g)&&" \
"(!a||!c||!d||!f||!h)&&(!a||!c||!d||!g||!h)&&(!a||!c||!e||!f||!g)&&(!a||!c||!e||!f||!h)&&" \
"(!a||!c||!e||!g||!h)&&(!a||!c||!f||!g||!h)&&(!a||!d||!e||!f||!g)&&(!a||!d||!e||!f||!h)&&" \
"(!a||!d||!e||!g||!h)&&(!a||!d||!f||!g||!h)&&(!a||!e||!f||!g||!h)&&(a||b||c||d||e)&&(a||b||c||d||f)&&" \
"(a||b||c||d||g)&&(a||b||c||d||h)&&(a||b||c||e||f)&&(a||b||c||e||g)&&(a||b||c||e||h)&&(a||b||c||f||g)&&" \
"(a||b||c||f||h)&&(a||b||c||g||h)&&(a||b||d||e||f)&&(a||b||d||e||g)&&(a||b||d||e||h)&&(a||b||d||f||g)&&" \
"(a||b||d||f||h)&&(a||b||d||g||h)&&(a||b||e||f||g)&&(a||b||e||f||h)&&(a||b||e||g||h)&&(a||b||f||g||h)&&" \
"(a||c||d||e||f)&&(a||c||d||e||g)&&(a||c||d||e||h)&&(a||c||d||f||g)&&(a||c||d||f||h)&&(a||c||d||g||h)&&" \
"(a||c||e||f||g)&&(a||c||e||f||h)&&(a||c||e||g||h)&&(a||c||f||g||h)&&(a||d||e||f||g)&&(a||d||e||f||h)&&" \
"(a||d||e||g||h)&&(a||d||f||g||h)&&(a||e||f||g||h)&&(!b||!c||!d||!e||!f)&&(!b||!c||!d||!e||!g)&&" \
"(!b||!c||!d||!e||!h)&&(!b||!c||!d||!f||!g)&&(!b||!c||!d||!f||!h)&&(!b||!c||!d||!g||!h)&&" \
"(!b||!c||!e||!f||!g)&&(!b||!c||!e||!f||!h)&&(!b||!c||!e||!g||!h)&&(!b||!c||!f||!g||!h)&&" \
"(!b||!d||!e||!f||!g)&&(!b||!d||!e||!f||!h)&&(!b||!d||!e||!g||!h)&&(!b||!d||!f||!g||!h)&&" \
"(!b||!e||!f||!g||!h)&&(b||c||d||e||f)&&(b||c||d||e||g)&&(b||c||d||e||h)&&(b||c||d||f||g)&&" \
"(b||c||d||f||h)&&(b||c||d||g||h)&&(b||c||e||f||g)&&(b||c||e||f||h)&&(b||c||e||g||h)&&" \
"(b||c||f||g||h)&&(b||d||e||f||g)&&(b||d||e||f||h)&&(b||d||e||g||h)&&(b||d||f||g||h)&&" \
"(b||e||f||g||h)&&(!c||!d||!e||!f||!g)&&(!c||!d||!e||!f||!h)&&(!c||!d||!e||!g||!h)&&" \
"(!c||!d||!f||!g||!h)&&(!c||!e||!f||!g||!h)&&(c||d||e||f||g)&&(c||d||e||f||h)&&(c||d||e||g||h)&&" \
"(c||d||f||g||h)&&(c||e||f||g||h)&&(!d||!e||!f||!g||!h)&&(d||e||f||g||h)"
return mathematica_to_CNF(s, a)

def POPCNT5 (a):
s="(!a||!b||!c||!d||!e||!f)&&(!a||!b||!c||!d||!e||!g)&&(!a||!b||!c||!d||!e||!h)&&" \
"(!a||!b||!c||!d||!f||!g)&&(!a||!b||!c||!d||!f||!h)&&(!a||!b||!c||!d||!g||!h)&&" \
"(!a||!b||!c||!e||!f||!g)&&(!a||!b||!c||!e||!f||!h)&&(!a||!b||!c||!e||!g||!h)&&" \
"(!a||!b||!c||!f||!g||!h)&&(!a||!b||!d||!e||!f||!g)&&(!a||!b||!d||!e||!f||!h)&&" \
"(!a||!b||!d||!e||!g||!h)&&(!a||!b||!d||!f||!g||!h)&&(!a||!b||!e||!f||!g||!h)&&" \
"(!a||!c||!d||!e||!f||!g)&&(!a||!c||!d||!e||!f||!h)&&(!a||!c||!d||!e||!g||!h)&&" \
"(!a||!c||!d||!f||!g||!h)&&(!a||!c||!e||!f||!g||!h)&&(!a||!d||!e||!f||!g||!h)&&" \
"(a||b||c||d)&&(a||b||c||e)&&(a||b||c||f)&&(a||b||c||g)&&(a||b||c||h)&&(a||b||d||e)&&" \
"(a||b||d||f)&&(a||b||d||g)&&(a||b||d||h)&&(a||b||e||f)&&(a||b||e||g)&&(a||b||e||h)&&" \
"(a||b||f||g)&&(a||b||f||h)&&(a||b||g||h)&&(a||c||d||e)&&(a||c||d||f)&&(a||c||d||g)&&" \
"(a||c||d||h)&&(a||c||e||f)&&(a||c||e||g)&&(a||c||e||h)&&(a||c||f||g)&&(a||c||f||h)&&" \
"(a||c||g||h)&&(a||d||e||f)&&(a||d||e||g)&&(a||d||e||h)&&(a||d||f||g)&&(a||d||f||h)&&" \
"(a||d||g||h)&&(a||e||f||g)&&(a||e||f||h)&&(a||e||g||h)&&(a||f||g||h)&&(!b||!c||!d||!e||!f||!g)&&" \
"(!b||!c||!d||!e||!f||!h)&&(!b||!c||!d||!e||!g||!h)&&(!b||!c||!d||!f||!g||!h)&&" \
"(!b||!c||!e||!f||!g||!h)&&(!b||!d||!e||!f||!g||!h)&&(b||c||d||e)&&(b||c||d||f)&&" \
"(b||c||d||g)&&(b||c||d||h)&&(b||c||e||f)&&(b||c||e||g)&&(b||c||e||h)&&(b||c||f||g)&&" \
"(b||c||f||h)&&(b||c||g||h)&&(b||d||e||f)&&(b||d||e||g)&&(b||d||e||h)&&(b||d||f||g)&&" \
"(b||d||f||h)&&(b||d||g||h)&&(b||e||f||g)&&(b||e||f||h)&&(b||e||g||h)&&(b||f||g||h)&&" \
"(!c||!d||!e||!f||!g||!h)&&(c||d||e||f)&&(c||d||e||g)&&(c||d||e||h)&&(c||d||f||g)&&" \
"(c||d||f||h)&&(c||d||g||h)&&(c||e||f||g)&&(c||e||f||h)&&(c||e||g||h)&&(c||f||g||h)&&" \
"(d||e||f||g)&&(d||e||f||h)&&(d||e||g||h)&&(d||f||g||h)&&(e||f||g||h)"
return mathematica_to_CNF(s, a)

def POPCNT6 (a):
s="(!a||!b||!c||!d||!e||!f||!g)&&(!a||!b||!c||!d||!e||!f||!h)&&(!a||!b||!c||!d||!e||!g||!h)&&" \
"(!a||!b||!c||!d||!f||!g||!h)&&(!a||!b||!c||!e||!f||!g||!h)&&(!a||!b||!d||!e||!f||!g||!h)&&" \
"(!a||!c||!d||!e||!f||!g||!h)&&(a||b||c)&&(a||b||d)&&(a||b||e)&&(a||b||f)&&(a||b||g)&&(a||b||h)&&" \
"(a||c||d)&&(a||c||e)&&(a||c||f)&&(a||c||g)&&(a||c||h)&&(a||d||e)&&(a||d||f)&&(a||d||g)&&(a||d||h)&&" \
"(a||e||f)&&(a||e||g)&&(a||e||h)&&(a||f||g)&&(a||f||h)&&(a||g||h)&&(!b||!c||!d||!e||!f||!g||!h)&&(b||c||d)&&" \
"(b||c||e)&&(b||c||f)&&(b||c||g)&&(b||c||h)&&(b||d||e)&&(b||d||f)&&(b||d||g)&&(b||d||h)&&(b||e||f)&&(b||e||g)&&" \
"(b||e||h)&&(b||f||g)&&(b||f||h)&&(b||g||h)&&(c||d||e)&&(c||d||f)&&(c||d||g)&&(c||d||h)&&(c||e||f)&&(c||e||g)&&" \
"(c||e||h)&&(c||f||g)&&(c||f||h)&&(c||g||h)&&(d||e||f)&&(d||e||g)&&(d||e||h)&&(d||f||g)&&(d||f||h)&&(d||g||h)&&" \
"(e||f||g)&&(e||f||h)&&(e||g||h)&&(f||g||h)"
return mathematica_to_CNF(s, a)

def POPCNT7 (a):
s="(!a||!b||!c||!d||!e||!f||!g||!h)&&(a||b)&&(a||c)&&(a||d)&&(a||e)&&(a||f)&&(a||g)&&(a||h)&&(b||c)&&" \
"(b||d)&&(b||e)&&(b||f)&&(b||g)&&(b||h)&&(c||d)&&(c||e)&&(c||f)&&(c||g)&&(c||h)&&(d||e)&&(d||f)&&(d||g)&&" \
"(d||h)&&(e||f)&&(e||g)&&(e||h)&&(f||g)&&(f||h)&&(g||h)"
return mathematica_to_CNF(s, a)

def POPCNT8 (a):
s="a&&b&&c&&d&&e&&f&&g&&h"
return mathematica_to_CNF(s, a)

POPCNT_functions=[POPCNT0, POPCNT1, POPCNT2, POPCNT3, POPCNT4, POPCNT5, POPCNT6, POPCNT7, POPCNT8]

def coords_to_var (row, col):
# we always use SAT variables as strings, anyway.
# the 1st variables is 1, not 0
return str(row*(WIDTH+2)+col+1)

def chk_bomb(row, col):
clauses=[]

# make empty border
# all variables are negated (because they must be False)
for c in range(WIDTH+2):
clauses.append ("-"+coords_to_var(0,c))
clauses.append ("-"+coords_to_var(HEIGHT+1,c))
for r in range(HEIGHT+2):
clauses.append ("-"+coords_to_var(r,0))
clauses.append ("-"+coords_to_var(r,WIDTH+1))

for r in range(1,HEIGHT+1):
for c in range(1,WIDTH+1):
t=known[r-1][c-1]
if t in "012345678":
# cell at r, c is empty (False):
clauses.append ("-"+coords_to_var(r,c))
# we need an empty border so the following expression would work for all possible cells:
neighbours=[coords_to_var(r-1, c-1), coords_to_var(r-1, c), coords_to_var(r-1, c+1), coords_to_var(r, c-1),
coords_to_var(r, c+1), coords_to_var(r+1, c-1), coords_to_var(r+1, c), coords_to_var(r+1, c+1)]
clauses=clauses+POPCNT_functions[int(t)](neighbours)

# place a bomb
clauses.append (coords_to_var(row,col))

f=open("tmp.cnf", "w")
f.write ("p cnf "+str(VARS_TOTAL)+" "+str(len(clauses))+"\n")
for c in clauses:
f.write(c+" 0\n")
f.close()

child = subprocess.Popen(["minisat", "tmp.cnf"], stdout=subprocess.PIPE)
child.wait()
# 10 is SAT, 20 is UNSAT
if child.returncode==20:
print "row=%d, col=%d, unsat!" % (row, col)

for r in range(1,HEIGHT+1):
for c in range(1,WIDTH+1):
if known[r-1][c-1]=="?":
chk_bomb(r, c)



The output CNF file can be large, up to ~2000 clauses, or more, here is an example: https://github.com/dennis714/yurichev.com/blob/master/blog/minesweeper_SAT/sample.cnf.

Anyway, it works just like my previous Z3Py script:

row=1, col=3, unsat!
row=6, col=2, unsat!
row=6, col=3, unsat!
row=7, col=4, unsat!
row=7, col=9, unsat!
row=8, col=9, unsat!


... but it runs way faster, even considering overhead of executing external program. Perhaps, Z3Py version could be optimized much better?

The files, including Wolfram Mathematica notebook: https://github.com/dennis714/yurichev.com/tree/master/blog/minesweeper_SAT.

→ [list of blog posts, my twitter/facebook]