12-Mar-2017: Conway’s Game of Life and SAT solver

(The following text has been copypasted to the SAT/SMT by example.)

Part I: reversing back state of "Game of Life".

How could we reverse back a known state of GoL? This can be solved by brute-force, but this is extremely slow and inefficient.

Let's try to use SAT solver.

First, we need to define a function which will tell, if the new cell will be created/born, preserved/stay or died. Quick refresher: cell is born if it has 3 neighbours, it stays alive if it has 2 or 3 neighbours, it dies in any other case.

This is how I can define a function reflecting state of a new cell in the next state:

if center==true:
return popcnt2(neighbours) || popcnt3(neighbours)
if center==false
return popcnt3(neighbours)


We can get rid of "if" construction:

result=(center=true && (popcnt2(neighbours) || popcnt3(neighbours))) || (center=false && popcnt3(neighbours))


... where "center" is state of central cell, "neighbours" are 8 neighbouring cells, popcnt2 is a function which returns True if it has exactly 2 bits on input, popcnt3 is the same, but for 3 bits (just like these were used in my "Minesweeper" example (https://yurichev.com/blog/minesweeper_SAT/)).

Using Wolfram Mathematica, I first create all helper functions and truth table for the function, which returns "true", if a cell must be present in the next state, or "false" if not:

In[1]:= popcount[n_Integer]:=IntegerDigits[n,2] // Total

In[2]:= popcount2[n_Integer]:=Equal[popcount[n],2]

In[3]:= popcount3[n_Integer]:=Equal[popcount[n],3]

In[4]:= newcell[center_Integer,neighbours_Integer]:=(center==1 && (popcount2[neighbours]|| popcount3[neighbours]))||
(center==0 && popcount3[neighbours])

Boole[newcell[center, neighbours]],{neighbours,0,255},{center,0,1}]]

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

...



Now we can create a CNF expression out of truth table:

In[14]:= BooleanConvert[BooleanFunction[NewCellIsTrue,{center,a,b,c,d,e,f,g,h}],"CNF"]
Out[14]= (!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)&&

...



Also, we need a second function, "inverted" one, which will return "true" if the cell must be absent in the next state, or "false" otherwise:

In[15]:= NewCellIsFalse=Flatten[Table[Join[{center},PadLeft[IntegerDigits[neighbours,2],8]] ->
Boole[Not[newcell[center, neighbours]]],{neighbours,0,255},{center,0,1}]]
Out[15]= {{0,0,0,0,0,0,0,0,0}->1,
{1,0,0,0,0,0,0,0,0}->1,
{0,0,0,0,0,0,0,0,1}->1,
{1,0,0,0,0,0,0,0,1}->1,
{0,0,0,0,0,0,0,1,0}->1,

...

In[16]:= BooleanConvert[BooleanFunction[NewCellIsFalse,{center,a,b,c,d,e,f,g,h}],"CNF"]
Out[16]= (!a||!b||!c||d||e||f||g||h)&&(!a||!b||c||!d||e||f||g||h)&&(!a||!b||c||d||!e||f||g||h)&&
(!a||!b||c||d||e||!f||g||h)&&(!a||!b||c||d||e||f||!g||h)&&(!a||!b||c||d||e||f||g||!h)&&
(!a||!b||!center||d||e||f||g||h)&&(!a||b||!c||!d||e||f||g||h)&&(!a||b||!c||d||!e||f||g||h)&&
(!a||b||!c||d||e||!f||g||h)&&(!a||b||!c||d||e||f||!g||h)&&(!a||b||!c||d||e||f||g||!h)&&
(!a||b||c||!d||!e||f||g||h)&&(!a||b||c||!d||e||!f||g||h)&&(!a||b||c||!d||e||f||!g||h)&&

...



Using the very same way as in my "Minesweeper" example, I can convert CNF expression to list of clauses:

def mathematica_to_CNF (s, center, a):
s=s.replace("center", center)
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


And again, as in "Minesweeper", there is an invisible border, to make processing simpler. SAT variables are also numbered as in previous example:

 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


Also, there is a visible border, always fixed to "False", to make things simpler.

Now the working source code. Whenever we encounter "*" in final_state[], we add clauses generated by cell_is_true() function, or cell_is_false() if otherwise. When we get a solution, it is negated and added to the list of clauses, so when minisat is executed next time, it will skip solution which was already printed.

...

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

return mathematica_to_CNF(s, center, a)

def cell_is_true (center, 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||center||d||e||f)&&(a||b||c||center||d||e||g)&&(a||b||c||center||d||e||h)&&" \
"(a||b||c||center||d||f||g)&&(a||b||c||center||d||f||h)&&(a||b||c||center||d||g||h)&&" \
"(a||b||c||center||e||f||g)&&(a||b||c||center||e||f||h)&&(a||b||c||center||e||g||h)&&" \
"(a||b||c||center||f||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||center||d||e||f||g)&&(a||b||center||d||e||f||h)&&" \
"(a||b||center||d||e||g||h)&&(a||b||center||d||f||g||h)&&(a||b||center||e||f||g||h)&&(a||b||d||e||f||g||h)&&" \
"(a||c||center||d||e||f||g)&&(a||c||center||d||e||f||h)&&(a||c||center||d||e||g||h)&&" \
"(a||c||center||d||f||g||h)&&(a||c||center||e||f||g||h)&&(a||c||d||e||f||g||h)&&(a||center||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||center||d||e||f||g)&&(b||c||center||d||e||f||h)&&(b||c||center||d||e||g||h)&&" \
"(b||c||center||d||f||g||h)&&(b||c||center||e||f||g||h)&&(b||c||d||e||f||g||h)&&(b||center||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||center||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, center, a)

...

( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/GoL_SAT/GoL_SAT_utils.py )
#!/usr/bin/python

import os
from GoL_SAT_utils import *

final_state=[
" * ",
"* *",
" * "]

H=len(final_state) # HEIGHT
W=len(final_state[0]) # WIDTH

print "HEIGHT=", H, "WIDTH=", W

VARS_TOTAL=W*H+1
VAR_FALSE=str(VARS_TOTAL)

def try_again (clauses):
# rules for the main part of grid
for r in range(H):
for c in range(W):
if final_state[r][c]=="*":
clauses=clauses+cell_is_true(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))
else:
clauses=clauses+cell_is_false(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))

# cells behind visible grid must always be false:
for c in range(-1, W+1):
for r in [-1,H]:
clauses=clauses+cell_is_false(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))
for c in [-1,W]:
for r in range(-1, H+1):
clauses=clauses+cell_is_false(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))

write_CNF("tmp.cnf", clauses, VARS_TOTAL)

print "%d clauses" % len(clauses)

solution=run_minisat ("tmp.cnf")
os.remove("tmp.cnf")
if solution==None:
print "unsat!"
exit(0)

grid=SAT_solution_to_grid(solution, H, W)

print_grid(grid)
write_RLE(grid)

return grid

clauses=[]
# always false:
clauses.append ("-"+VAR_FALSE)

while True:
solution=try_again(clauses)
clauses.append(negate_clause(grid_to_clause(solution, H, W)))
print ""


( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/GoL_SAT/reverse1.py )

Here is a result:

HEIGHT= 3 WIDTH= 3
2525 clauses
.*.
*.*
.*.
1.rle written

2526 clauses
.**
*..
*.*
2.rle written

2527 clauses
**.
..*
*.*
3.rle written

2528 clauses
*.*
*..
.**
4.rle written

2529 clauses
*.*
..*
**.
5.rle written

2530 clauses
*.*
.*.
*.*
6.rle written

2531 clauses
unsat!


The first result is the same as input state. Indeed: this is "still life", i.e., state which will never change, and it is correct solution. The last solution is also valid.

Now the problem: 2nd, 3rd, 4th and 5th solutions are equivalent to each other, they just mirrored or rotated. In fact, this is reflectional (like in mirror) and rotational symmetries. We can solve this easily: we will take each solution, reflect and rotate it and add them negated to the list of clauses, so minisat will skip them during its work:


...

while True:
solution=try_again(clauses)
clauses.append(negate_clause(grid_to_clause(solution, H, W)))
clauses.append(negate_clause(grid_to_clause(reflect_vertically(solution), H, W)))
clauses.append(negate_clause(grid_to_clause(reflect_horizontally(solution), H, W)))
# is this square?
if W==H:
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,1), H, W)))
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,2), H, W)))
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,3), H, W)))
print ""

...


( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/GoL_SAT/reverse2.py )

Functions reflect_vertically(), reflect_horizontally and rotate_square_array() are simple array manipulation routines.

Now we get just 3 solutions:

HEIGHT= 3 WIDTH= 3
2525 clauses
.*.
*.*
.*.
1.rle written

2531 clauses
.**
*..
*.*
2.rle written

2537 clauses
*.*
.*.
*.*
3.rle written

2543 clauses
unsat!


This one has only one single ancestor:

final_state=[
" * ",
" * ",
" * "]

HEIGHT= 3 WIDTH= 3
2503 clauses
...
***
...
1.rle written

2509 clauses
unsat!


This is oscillator, of course.

How many states can lead to such picture?

final_state=[
"  *  ",
"     ",
" **  ",
"  *  ",
"  *  ",
" *** "]


28, these are few:

HEIGHT= 6 WIDTH= 5
5217 clauses
.*.*.
..*..
.**.*
..*..
..*.*
.**..
1.rle written

5220 clauses
.*.*.
..*..
.**.*
..*..
*.*.*
.**..
2.rle written

5223 clauses
..*.*
..**.
.**..
....*
*.*.*
.**..
3.rle written

5226 clauses
..*.*
..**.
.**..
*...*
..*.*
.**..
4.rle written

...



final_state=[
"             ",
"   *     *   ",
"    *   *    ",
"   *******   ",
"  ** *** **  ",
" *********** ",
" * ******* * ",
" * *     * * ",
"    ** **    ",
"             "]

HEIGHT= 10 WIDTH= 13
16469 clauses
..*.*.**.....
.....*****...
....**..*....
......*...*..
..**...*.*...
.*..*.*.**..*
*....*....*.*
..*.*..*.....
..*.....*.*..
....**..*.*..
1.rle written

16472 clauses
*.*.*.**.....
.....*****...
....**..*....
......*...*..
..**...*.*...
.*..*.*.**..*
*....*....*.*
..*.*..*.....
..*.....*.*..
....**..*.*..
2.rle written

16475 clauses
..*.*.**.....
*....*****...
....**..*....
......*...*..
..**...*.*...
.*..*.*.**..*
*....*....*.*
..*.*..*.....
..*.....*.*..
....**..*.*..
3.rle written

...



I don't know how many possible input states can lead to "space invader", perhaps, too many. Had to stop it. And it slows down during execution, because number of clauses is increasing (because of negating solutions addition).

All solutions are also exported to RLE files, which can be opened by Golly (http://golly.sourceforge.net/) software.

Part II: finding "still lives"

"Still life" in terms of GoL is a state which doesn't change at all.

First, using previous definitions, we will define a truth table of function, which will return true, if the center cell of the next state is the same as it has been in the previous state, i.e., hasn't been changed:

In[17]:= stillife=Flatten[Table[Join[{center},PadLeft[IntegerDigits[neighbours,2],8]]->
Boole[Boole[newcell[center,neighbours]]==center],{neighbours,0,255},{center,0,1}]]
Out[17]= {{0,0,0,0,0,0,0,0,0}->1,
{1,0,0,0,0,0,0,0,0}->0,
{0,0,0,0,0,0,0,0,1}->1,
{1,0,0,0,0,0,0,0,1}->0,

...

In[18]:= BooleanConvert[BooleanFunction[stillife,{center,a,b,c,d,e,f,g,h}],"CNF"]
Out[18]= (!a||!b||!c||!center||!d)&&(!a||!b||!c||!center||!e)&&(!a||!b||!c||!center||!f)&&
(!a||!b||!c||!center||!g)&&(!a||!b||!c||!center||!h)&&(!a||!b||!c||center||d||e||f||g||h)&&
(!a||!b||c||center||!d||e||f||g||h)&&(!a||!b||c||center||d||!e||f||g||h)&&(!a||!b||c||center||d||e||!f||g||h)&&
(!a||!b||c||center||d||e||f||!g||h)&&(!a||!b||c||center||d||e||f||g||!h)&&(!a||!b||!center||!d||!e)&&

...


#!/usr/bin/python

import os
from GoL_SAT_utils import *

W=3 # WIDTH
H=3 # HEIGHT

VARS_TOTAL=W*H+1
VAR_FALSE=str(VARS_TOTAL)

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

return mathematica_to_CNF(s, center, a)

def try_again (clauses):
# rules for the main part of grid
for r in range(H):
for c in range(W):
clauses=clauses+stillife(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))

# cells behind visible grid must always be false:
for c in range(-1, W+1):
for r in [-1,H]:
clauses=clauses+cell_is_false(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))
for c in [-1,W]:
for r in range(-1, H+1):
clauses=clauses+cell_is_false(coords_to_var(r, c, H, W), get_neighbours(r, c, H, W))

write_CNF("tmp.cnf", clauses, VARS_TOTAL)

print "%d clauses" % len(clauses)

solution=run_minisat ("tmp.cnf")
os.remove("tmp.cnf")
if solution==None:
print "unsat!"
exit(0)

grid=SAT_solution_to_grid(solution, H, W)
print_grid(grid)
write_RLE(grid)

return grid

clauses=[]
# always false:
clauses.append ("-"+VAR_FALSE)

while True:
solution=try_again(clauses)
clauses.append(negate_clause(grid_to_clause(solution, H, W)))
clauses.append(negate_clause(grid_to_clause(reflect_vertically(solution), H, W)))
clauses.append(negate_clause(grid_to_clause(reflect_horizontally(solution), H, W)))
# is this square?
if W==H:
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,1), H, W)))
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,2), H, W)))
clauses.append(negate_clause(grid_to_clause(rotate_square_array(solution,3), H, W)))
print ""



What we've got for 2*2?

1881 clauses
..
..
1.rle written

1887 clauses
**
**
2.rle written

1893 clauses
unsat!


Both solutions are correct: empty square will progress into empty square (no cells are born). 2*2 box is also known still life.

2887 clauses
...
...
...
1.rle written

2893 clauses
.**
.**
...
2.rle written

2899 clauses
.**
*.*
**.
3.rle written

2905 clauses
.*.
*.*
**.
4.rle written

2911 clauses
.*.
*.*
.*.
5.rle written

2917 clauses
unsat!


Here is a problem: we see familiar 2*2 box, but shifted. This is indeed correct solution, but we don't interested in it, because it has been already seen.

What we can do is add another condition. We can force minisat to find solutions with no empty rows and columns. This is easy. These are SAT variables for 5*5 square:

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


Each clause is "OR" clause, so all we have to do is to add 5 clauses:

1 OR 2 OR 3 OR 4 OR 5
6 OR 7 OR 8 OR 9 OR 10

...



That means that each row must have at least one "True" variable somewhere. We can also do this for each column as well.


...

# each row must contain at least one cell!
for r in range(H):
clauses.append(" ".join([coords_to_var(r, c, H, W) for c in range(W)]))

# each column must contain at least one cell!
for c in range(W):
clauses.append(" ".join([coords_to_var(r, c, H, W) for r in range(H)]))

...


( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/GoL_SAT/stillife2.py )

Now we can see that 3*3 square has 3 possible still lives:

2893 clauses
.*.
*.*
**.
1.rle written

2899 clauses
.*.
*.*
.*.
2.rle written

2905 clauses
.**
*.*
**.
3.rle written

2911 clauses
unsat!


4*4 has 7:

4169 clauses
..**
...*
***.
*...
1.rle written

4175 clauses
..**
..*.
*.*.
**..
2.rle written

4181 clauses
..**
.*.*
*.*.
**..
3.rle written

4187 clauses
..*.
.*.*
*.*.
**..
4.rle written

4193 clauses
.**.
*..*
*.*.
.*..
5.rle written

4199 clauses
..*.
.*.*
*.*.
.*..
6.rle written

4205 clauses
.**.
*..*
*..*
.**.
7.rle written

4211 clauses
unsat!


When I try large squares, like 20*20, funny things happen. First of all, minisat finds solutions not very pleasing aesthetically, but still correct, like:

61033 clauses
....**.**.**.**.**.*
**..*.**.**.**.**.**
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
..*.................
...*................
***.................
*...................
1.rle written

...



Indeed: all rows and columns has at least one "True" variable.

Then minisat begins to add smaller "still lives" into the whole picture:

61285 clauses
.**....**...**...**.
.**...*..*.*.*...*..
.......**...*......*
..................**
...**............*..
...*.*...........*..
....*.*........**...
**...*.*...**..*....
*.*...*....*....*...
.*..........****.*..
................*...
..*...**..******....
.*.*..*..*..........
*..*...*.*..****....
***.***..*.*....*...
....*..***.**..**...
**.*..*.............
.*.**.**..........**
*..*..*..*......*..*
**..**..**......**..
43.rle written


In other words, result is a square consisting of smaller "still lives". It then altering these parts slightly, shifting back and forth. Is it cheating? Anyway, it does it in a strict accordance to rules we defined.

But we want "denser" picture. We can add a rule: in all 5-cell chunks there must be at least one "True" cell. To achieve this, we just split the whole square by 5-cell chunks and add clause for each:


...

# make result denser:
lst=[]
for r in range(H):
for c in range(W):
lst.append(coords_to_var(r, c, H, W))
# divide them all by chunks and add to clauses:
CHUNK_LEN=5
for c in list_partition(lst,len(lst)/CHUNK_LEN):
tmp=" ".join(c)
clauses.append(tmp)

...


( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/GoL_SAT/stillife.py )

This is indeed denser:

61113 clauses
..**.**......*.*.*..
...*.*.....***.**.*.
...*..*...*.......*.
....*.*..*.*......**
...**.*.*..*...**.*.
..*...*.***.....*.*.
...*.*.*......*..*..
****.*..*....*.**...
*....**.*....*.*....
...**..*...**..*....
..*..*....*....*.**.
.*.*.**....****.*..*
..*.*....*.*..*..**.
....*.****..*..*.*..
....**....*.*.**..*.
*.**...****.*..*.**.
**...**.....**.*....
...**..*..**..*.**.*
***.*.*..*.*..*.*.**
*....*....*....*....
1.rle written

61119 clauses
..**.**......*.*.*..
...*.*.....***.**.*.
...*..*...*.......*.
....*.*..*.*......**
...**.*.*..*...**.*.
..*...*.***.....*.*.
...*.*.*......*..*..
****.*..*....*.**...
*....**.*....*.*....
...**..*...**..*....
..*..*....*....*.**.
.*.*.**....****.*..*
..*.*....*.*..*..**.
....*.****..*..*.*..
....**....*.*.**..*.
*.**...****.*..*.**.
**...**.....**.*....
...**..*.***..*.**.*
***.*..*.*..*.*.*.**
*.......*..**.**....
2.rle written

...



Let's try more dense, one mandatory "true" cell per each 4-cell chunk:

61133 clauses
.**.**...*....**..**
*.*.*...*.*..*..*..*
*....*...*.*..*.**..
.***.*.....*.**.*...
..*.*.....**...*..*.
*......**..*...*.**.
**.....*...*.**.*...
...**...*...**..*...
**.*..*.*......*...*
.*...**.**..***.****
.*....*.*..*..*.*...
**.***...*.**...*.**
.*.*..****.....*..*.
*....*.....**..**.*.
*.***.*..**.*.....**
.*...*..*......**...
...*.*.**......*.***
..**.*.....**......*
*..*.*.**..*.*..***.
**....*.*...*...*...
1.rle written

61139 clauses
.**.**...*....**..**
*.*.*...*.*..*..*..*
*....*...*.*..*.**..
.***.*.....*.**.*...
..*.*.....**...*..*.
*......**..*...*.**.
**.....*...*.**.*...
...**...*...**..*...
**.*..*.*......*...*
.*...**.**..***.****
.*....*.*..*..*.*...
**.***...*.**...*.**
.*.*..****.....*..*.
*....*.....**..**.*.
*.***.*..**.*.....**
.*...*..*......**..*
...*.*.**......*.**.
..**.*.....**....*..
*..*.*.**..*.*...*.*
**....*.*...*.....**
2.rle written

...



... and even more: one cell per each 3-cell chunk:

61166 clauses
**.*..**...**.**....
*.**..*.*...*.*.*.**
....**..*...*...*.*.
.**..*.*.**.*.*.*.*.
..**.*.*...*.**.*.**
*...*.*.**.*....*.*.
**.*..*...*.*.***..*
.*.*.*.***..**...**.
.*.*.*.*..**...*.*..
**.**.*..*...**.*..*
..*...*.**.**.*.*.**
..*.**.*..*.*.*.*...
**.*.*...*..*.*.*...
.*.*...*.**..*..***.
.*..****.*....**...*
..*.*...*..*...*..*.
.**...*.*.**...*.*..
..*..**.*.*...**.**.
..*.*..*..*..*..*..*
.**.**....**..**..**
1.rle written

61172 clauses
**.*..**...**.**....
*.**..*.*...*.*.*.**
....**..*...*...*.*.
.**..*.*.**.*.*.*.*.
..**.*.*...*.**.*.**
*...*.*.**.*....*.*.
**.*..*...*.*.***..*
.*.*.*.***..**...**.
.*.*.*.*..**...*.*..
**.**.*..*...**.*..*
..*...*.**.**.*.*.**
..*.**.*..*.*.*.*...
**.*.*...*..*.*.*...
.*.*...*.**..*..***.
.*..****.*....**...*
..*.*...*..*...*..*.
.**..**.*.**...*.*..
*..*.*..*.*...**.**.
*..*.*.*..*..*..*..*
.**...*...**..**..**
2.rle written

...



This is most dense. Unfortunaly, it's impossible to construct "still life" with one mandatory "true" cell per each 2-cell chunk.

Source code

Source code and Wolfram Mathematica notebook: https://github.com/DennisYurichev/yurichev.com/tree/master/blog/GoL_SAT.