B4-S4 is a SAT-based oscillator finder of Conway's game of life under rule B4/S4.

Given a $n\times m$ table, each grid can be either alive of dead, it is called the state at time $0$, and given the state at time $t$, the state at time $t+1$ is followed by the rules

• if there are exactly 4 of a cell's neighbors are alive at $t$, then the cell is alive at $t+1$.
• otherwise, the cell is dead at $t+1$.

where the neighbors of a cell at coordinate $(x,y)$ is defined by $$ N_{(x,y)}={(a,b)\mid |x-a|,|y-b|\leq 1}\setminus{(x,y)} $$ namely the 8 cells nearly the cell $(x,y)$.

we call the initial state $S_0$, its next state $S_1$ followed by the rule, and $S_2,S_3,\ldots$ and so on. An oscillator is a state $O_0$ if

• $O_0$ is nonempty
• $O_0=O_t$ for some positive integer $t$

if such $t$ is the minimum number satisfying the condition, then $t$ is called the period. The following figures shows an example of oscillator of period $2$.

$O_0$	$O_1$	$O_2$

And the problem we interests is to find out all oscillator or find a general way to construct oscillator.

Given boolean variables $x_1,x_2,\ldots,x_n$, an boolean expression is called CNF if it is in the form $$ F(x_1,\ldots,x_n)=\bigwedge\left(\bigvee x_i\right) $$

and to find an assignment of $x_1,\ldots x_n$ is called SAT problem. It is an NP-complete problem, but with some efficient algorithm, we can solve it with quite good large number. Also, the aim of the program is to reduct the oscillator finding to an CNF and solve it by SAT solver called MiniSat.

• Unlike original Game of Life, the rule ensure the cells won't exceed the original margin, namely $n\times m$.
• Unlike original Game of Life, there is no Still lifes, namely oscillator with period $1$.

The smallest oscillator is in size $7\times7$, we called fire

fire0	fire1

For $8\times8$, there are $4$ types of oscillator.

	time 0	time 1
Crystal
Currency
Face
Robot

For $8\times9$, there are 2 types.

	time 0	time 1
Deer
Shuriken

And further we have some complicated and not well-symmetrical oscillators. The number of oscillator increases rapidly when the size comes to $12$. Here are some examples.

	time 0	time 1
Girrafe
Parallelogram
Tilt

There are infinitely many oscillators, since we can repeat this pattern for any finite times

time 0	time 1

• all oscillators are with period 2