\myheading{Finding ``still lives''}

\leveldown{}

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

\myheading{... using SAT-solver}

First, using previous definitions, we will define a truth table of function, which will return \emph{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:

\begin{lstlisting}
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)&&

...

\end{lstlisting}

\lstinputlisting[style=custompy]{\CURPATH/SL1.py}

( \url{\RepoURL/\CURPATH/SL1.py} )

What we've got for $2 \cdot 2$?

\begin{lstlisting}
..
..
1.rle written

**
**
2.rle written

unsat!
\end{lstlisting}

Both solutions are correct: empty square will progress into empty square (no cells are born).
$2 \cdot 2$ box is also known ``still life''.

What about $3 \cdot 3$ square?

\begin{lstlisting}
...
...
...
1.rle written

.**
.**
...
2.rle written

.**
*.*
**.
3.rle written

.*.
*.*
**.
4.rle written

.*.
*.*
.*.
5.rle written

unsat!
\end{lstlisting}

Here is a problem: we see familiar $2 \cdot 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 \cdot 5$ square:

\begin{lstlisting}
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
\end{lstlisting}

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

\begin{lstlisting}
1 OR 2 OR 3 OR 4 OR 5
6 OR 7 OR 8 OR 9 OR 10

...

\end{lstlisting}

That means that each row must have at least one \emph{True} value somewhere.
We can also do this for each column as well.

\begin{lstlisting}

...

    # 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)]))

...

\end{lstlisting}

( \url{\RepoURL/\CURPATH/SL2.py} )

Now we can see that $3 \cdot 3$ square has 3 possible ``still lives'':

\begin{lstlisting}
.*.
*.*
**.
1.rle written

.*.
*.*
.*.
2.rle written

.**
*.*
**.
3.rle written

unsat!
\end{lstlisting}

$4 \cdot 4$ has 7:

\begin{lstlisting}
..**
...*
***.
*...
1.rle written

..**
..*.
*.*.
**..
2.rle written

..**
.*.*
*.*.
**..
3.rle written

..*.
.*.*
*.*.
**..
4.rle written

.**.
*..*
*.*.
.*..
5.rle written

..*.
.*.*
*.*.
.*..
6.rle written

.**.
*..*
*..*
.**.
7.rle written

unsat!
\end{lstlisting}

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

\begin{lstlisting}
....**.**.**.**.**.*
**..*.**.**.**.**.**
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
**..................
*...................
.*..................
..*.................
...*................
***.................
*...................
1.rle written

...

\end{lstlisting}

Indeed: all rows and columns has at least one \emph{True} value.

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

\begin{lstlisting}
.**....**...**...**.
.**...*..*.*.*...*..
.......**...*......*
..................**
...**............*..
...*.*...........*..
....*.*........**...
**...*.*...**..*....
*.*...*....*....*...
.*..........****.*..
................*...
..*...**..******....
.*.*..*..*..........
*..*...*.*..****....
***.***..*.*....*...
....*..***.**..**...
**.*..*.............
.*.**.**..........**
*..*..*..*......*..*
**..**..**......**..
43.rle written
\end{lstlisting}

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.

However, when I switch to Parallel Lingeling, things are slightly different:

\begin{lstlisting}
...............**.**
...............*...*
....**..**.**...**..
.....*...*.*..*.*...
.....*.*.*.*.**.*...
...**.*.*...*..*....
..*.*.*......**.....
..**...*............
........*...........
.........*..........
..........*.........
...........*........
............*...**..
.............*..*...
..............*.*...
...............*....
.**.................
..*.................
*...................
**..................
2.rle written
\end{lstlisting}

It's still correct.

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

\begin{lstlisting}

...

    # make result denser:
    lst=[]
    for r in range(H):
        for c in range(W):
            lst.append(GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W))
    # divide them all by chunks and add to clauses:
    CHUNK_LEN=3
    for c in my_utils.partition(lst,int(len(lst)/CHUNK_LEN)):
        s.add_clause(c)

...

\end{lstlisting}

( \url{\RepoURL/\CURPATH/SL3.py} )

This is indeed denser:

\begin{lstlisting}
..**.**......*.*.*..
...*.*.....***.**.*.
...*..*...*.......*.
....*.*..*.*......**
...**.*.*..*...**.*.
..*...*.***.....*.*.
...*.*.*......*..*..
****.*..*....*.**...
*....**.*....*.*....
...**..*...**..*....
..*..*....*....*.**.
.*.*.**....****.*..*
..*.*....*.*..*..**.
....*.****..*..*.*..
....**....*.*.**..*.
*.**...****.*..*.**.
**...**.....**.*....
...**..*..**..*.**.*
***.*.*..*.*..*.*.**
*....*....*....*....
1.rle written

..**.**......*.*.*..
...*.*.....***.**.*.
...*..*...*.......*.
....*.*..*.*......**
...**.*.*..*...**.*.
..*...*.***.....*.*.
...*.*.*......*..*..
****.*..*....*.**...
*....**.*....*.*....
...**..*...**..*....
..*..*....*....*.**.
.*.*.**....****.*..*
..*.*....*.*..*..**.
....*.****..*..*.*..
....**....*.*.**..*.
*.**...****.*..*.**.
**...**.....**.*....
...**..*.***..*.**.*
***.*..*.*..*.*.*.**
*.......*..**.**....
2.rle written

...

\end{lstlisting}

Let's try more dense, one mandatory \emph{true} cell per each 4-cell chunk:

\begin{lstlisting}
.**.**...*....**..**
*.*.*...*.*..*..*..*
*....*...*.*..*.**..
.***.*.....*.**.*...
..*.*.....**...*..*.
*......**..*...*.**.
**.....*...*.**.*...
...**...*...**..*...
**.*..*.*......*...*
.*...**.**..***.****
.*....*.*..*..*.*...
**.***...*.**...*.**
.*.*..****.....*..*.
*....*.....**..**.*.
*.***.*..**.*.....**
.*...*..*......**...
...*.*.**......*.***
..**.*.....**......*
*..*.*.**..*.*..***.
**....*.*...*...*...
1.rle written

.**.**...*....**..**
*.*.*...*.*..*..*..*
*....*...*.*..*.**..
.***.*.....*.**.*...
..*.*.....**...*..*.
*......**..*...*.**.
**.....*...*.**.*...
...**...*...**..*...
**.*..*.*......*...*
.*...**.**..***.****
.*....*.*..*..*.*...
**.***...*.**...*.**
.*.*..****.....*..*.
*....*.....**..**.*.
*.***.*..**.*.....**
.*...*..*......**..*
...*.*.**......*.**.
..**.*.....**....*..
*..*.*.**..*.*...*.*
**....*.*...*.....**
2.rle written

...

\end{lstlisting}

\dots and even more: one cell per each 3-cell chunk:

\begin{lstlisting}
**.*..**...**.**....
*.**..*.*...*.*.*.**
....**..*...*...*.*.
.**..*.*.**.*.*.*.*.
..**.*.*...*.**.*.**
*...*.*.**.*....*.*.
**.*..*...*.*.***..*
.*.*.*.***..**...**.
.*.*.*.*..**...*.*..
**.**.*..*...**.*..*
..*...*.**.**.*.*.**
..*.**.*..*.*.*.*...
**.*.*...*..*.*.*...
.*.*...*.**..*..***.
.*..****.*....**...*
..*.*...*..*...*..*.
.**...*.*.**...*.*..
..*..**.*.*...**.**.
..*.*..*..*..*..*..*
.**.**....**..**..**
1.rle written

**.*..**...**.**....
*.**..*.*...*.*.*.**
....**..*...*...*.*.
.**..*.*.**.*.*.*.*.
..**.*.*...*.**.*.**
*...*.*.**.*....*.*.
**.*..*...*.*.***..*
.*.*.*.***..**...**.
.*.*.*.*..**...*.*..
**.**.*..*...**.*..*
..*...*.**.**.*.*.**
..*.**.*..*.*.*.*...
**.*.*...*..*.*.*...
.*.*...*.**..*..***.
.*..****.*....**...*
..*.*...*..*...*..*.
.**..**.*.**...*.*..
*..*.*..*.*...**.**.
*..*.*.*..*..*..*..*
.**...*...**..**..**
2.rle written

...

\end{lstlisting}

This is most dense. Unfortunately, it's impossible to construct ``still life'' with one mandatory 
\emph{true} cell per each 2-cell chunk.

\myheading{... using MaxSAT-solver: getting maximum density still life}

Using Open-WBO MaxSAT solver,
it can find a $13 \cdot 13$ still life for ~11 minutes on my ancient Intel Xeon E3-1220 @ 3.10GHz.

\begin{lstlisting}
cells: 90
density: 0.532544
**.**.*.**.**
**.*.***.*.**
...*.....*...
****.**.*.***
*...*.*.*...*
.*.*..*.**.*.
**.**.*..*.**
.*.*..**.*.*.
*..*.*...*..*
****.****.***
.........*...
**.**.**.*.**
**.**.**.**.*
\end{lstlisting}

(Open-WBO has been switched to the fastest algorithm for the task, "LinearSU" (1st one).

I just maximize all cells, adding them as soft clauses:

\begin{lstlisting}
...

for r in range(H):
    for c in range(W):
        s.add_soft_clause([GoL_SAT_utils.coords_to_var(grid, VAR_FALSE, r, c, H, W)], 1)

...
\end{lstlisting}

( \url{\RepoURL/\CURPATH/SL_MaxSAT.py} )

See also:

\begin{itemize}
\item \href{http://csplib.org/Problems/prob032/}{CSPLIB Problem 032: Maximum density still life}

\item \href{http://www.ai.sri.com/~nysmith/life/index.html}{Maximum Density Still Life}

\item Also, an interesting paper:
Chu, G., \& Stuckey, P. J. (2012). A complete solution to the Maximum Density Still Life Problem. Artificial Intelligence, 184-185, 1–16. doi:10.1016/j.artint.2012.02.001
\end{itemize}

Further work: count solutions, eliminating symmetrical.
Search for symmetrical still lives, like:
\url{https://www.conwaylife.com/wiki/Clips},
\url{https://www.conwaylife.com/wiki/Inflected_clips}.

\levelup{}