This is what I did before with Z3, see here (Ctrl-F "Minesweeper").
The SAT version of this program used Mathematica-generated POPCNT functions.
Now what if I locked on a desert island again, with no Internet and Wolfram Mathematica?
Here is another way of solving it using SAT solver. The main problem is to count bits around a cell.
Here I described sorting networks shortly. They are popular in GPU, because they can be parallelized easily to work on multiple CPU cores.
They can be used for sorting boolean values. 01101 will become 00111, 10001 -> 00011, etc. We will count bits using sorting network.
My implementation is a simplest "bubble sort" and not the one the most optimized I described earlier. It's created recursively, as shown in Wikipedia:
The resulting 6-wire network is:
Now the comparator/swapper. How do we compare/swap two boolean variables, A and B?
A B out1 out2 0 0 0 0 0 1 0 1 1 0 0 1 1 1 1 1
As you can deduce effortlessly, out1 is just an AND, out2 is OR.
And here is all functions creating sorting network in my SAT_lib Python library:
def sort_unit(self, a, b):
return self.OR_list([a,b]), self.AND(a,b)
def sorting_network_make_ladder(self, lst):
if len(lst)==2:
return list(self.sort_unit(lst[0], lst[1]))
tmp=self.sorting_network_make_ladder(lst[1:]) # lst without head
first, second=self.sort_unit(lst[0], tmp[0])
return [first, second] + tmp[1:]
def sorting_network(self, lst):
# simplest possible, bubble sort
if len(lst)==2:
return self.sorting_network_make_ladder(lst)
tmp=self.sorting_network_make_ladder(lst)
return self.sorting_network(tmp[:-1]) + [tmp[-1]]
( https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/libs/SAT_lib.py )
Now if you will look closely on the output of sorting network, it looks like a thermometer, isn't it? This is indeed "unary coding", or "thermometer code", where 1 is encoded as 1, 2 as 11... 4 as 1111, etc. Who need such a wasteful code? For 9 inputs/outputs, we can afford it so far.
In other words, sorting network is a device counting input bits and giving output in unary coding.
Also, we don't need to add 9 constraints for each variable. Only two will suffice, one False and one True, because we are only interesting in the "level" of a thermometer.
def POPCNT(s, n, vars):
sorted=s.sorting_network(vars)
s.fix_always_false(sorted[n])
if n!=0:
s.fix_always_true(sorted[n-1])
And the whole source code:
#!/usr/bin/python
import SAT_lib
WIDTH=9
HEIGHT=9
VARS_TOTAL=(WIDTH+2)*(HEIGHT+2)
known=[
"01?10001?",
"01?100011",
"011100000",
"000000000",
"111110011",
"????1001?",
"????3101?",
"?????211?",
"?????????"]
def POPCNT(s, n, vars):
sorted=s.sorting_network(vars)
s.fix_always_false(sorted[n])
if n!=0:
s.fix_always_true(sorted[n-1])
def chk_bomb(row, col):
s=SAT_lib.SAT_lib(False)
vars=[[s.create_var() for c in range(WIDTH+2)] for r in range(HEIGHT+2)]
# make empty border
# all variables are negated (because they must be False)
for c in range(WIDTH+2):
s.fix_always_false(vars[0][c])
s.fix_always_false(vars[HEIGHT+1][c])
for r in range(HEIGHT+2):
s.fix_always_false(vars[r][0])
s.fix_always_false(vars[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):
s.fix_always_false(vars[r][c])
# we need an empty border so the following expression would work for all possible cells:
neighbours=[vars[r-1][c-1], vars[r-1][c], vars[r-1][c+1], vars[r][c-1],
vars[r][c+1], vars[r+1][c-1], vars[r+1][c], vars[r+1][c+1]]
POPCNT(s, int(t), neighbours)
# place a bomb
s.fix_always_true (vars[row][col])
if s.solve()==False:
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)
As before, this is a list of Minesweeper cells you can safely click on:
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!
However, it works several times slower than the version with Mathematica-generated POPCNT functions, which is the fastest version so far...
Nevertheless, sorting networks has important place in SAT/SMT world. By fixing a "level" of a thermometer using a single constraint, it's possible to add PB (pseudo-boolean) constraints, like, "x>=10" (you need just to force a "level" to be always higher or equal than 10).