This post is based on the final project I did with Tenzin Low in CSE 507 (computer-aided reasoning for software).

Conway's Game of Life is a model of a population of organisms that live and die on a grid according to a set of simple rules:

1. A dead cell with exactly three live neighbors becomes a live cell and stays dead otherwise.
2. A live cell with two or three live neighbors lives on and dies otherwise.

All kinds of amazing shuffling, oscillating, and stationary patterns emerge.

Satisfiability Modulo Theories (SMT) solvers, such as Z3, determine the satisfiability of a set of constraints. For example, They are often used to solve problems in software verification, such as finding programs that satisfy a specification or verifying that a program satisfies a specification. We can think of the rules and state of Life as programs and use an SMT solver to synthesize states and rules for Life that follow desired behavior.

The encoding: booleans or integers?

First, we need a symbolic encoding of Life that Z3 understands. Finitizing the state, let's say we're simulating A natural choice would be to represent State can be encoded as a 3D grid (width by height by time steps) of Z3 integers, constrained to be 0 (dead) or 1 (alive). To encode the transition function, we add a constraint for each cell position between consecutive times according to typical transition rules:

Tenzin and I did some scaling experiments and found that using constrained integers leads to faster solve times than using booleans with pseudo-boolean constraints. This is strange because pseudo-boolean constraints such as PbEq t. However, Z3 does have a tactic to re-encode 0/1-constrained integers using bitvectors and then invoke a bit-blasting solver. My guess is that the point of pseudo-boolean constraints is more about expresstivity.

Ok actually I investigated this, I think PB uses SMT theory while pb2bv uses the SAT solver

Searching backwards

What pattern leads to the smiley face after two steps? Press the Invert button to find out (pressing this button for the first time will download a 7MB file containing the Z3 solver). You can also click to create a target pattern on the left side and adjust the number of steps to search backwards. On the right side, sat means the solver found a solution, and unsat means it didn't.

Once we have a symbolic encoding of Life, inverting it with Z3 is pretty straightforward by adding constraints that the target pattern is the final state. With a finitized grid, we also need to add constraints that each state would not cause cells outside the boundary to become alive. In pseudocode, this looks like

for i, j in cells:
    solver.add(vars[-1][i][j] == target[i][j]);

for t in range(steps):
    for i in range(1, width - 1):
        solver.add(vars[t][i - 1][0] + vars[t][i][0] + vars[t][i + 1][0] != 3);
        # similar for other edges

where vars is a 3D array of boolean variables representing the state of each cell at each step.

You might also wonder if there are states with no predecessors—these are called Garden of Eden. We tried using Z3 to find Gardens by iterating over all states of a given size and searching backwards, but it was too slow, although using incremental solving (maintaining constraints and information between calls to the solver) did get a speedup.

Synthesizing spaceships, oscillators, and still life

for i, j in cells:
    solver.add(vars[0][i][j] == vars[period][i + dy][j + dx]);

for t in range(2, period):
    if period % t == 0:
        solver.add(vars[t][i][j] != vars[t][i + dy][j + dx]);

Suggested parameters:

• Spaceship
  • Glider: size = 3, period = 4, \(|dx|\) = \(|dy|\) = 1
  • Lightweight spaceship: size = 5, period = 4, \(|dx|\) = 2 and \(|dy|\) = 0 or \(|dx|\) = 0 and \(|dy|\) = 2
• Oscillators (\(dx\) = \(dy\) = 0)
  • Blinker: size = 3, period = 2
  • Mold: size = 6, period = 4
  • Jam: size = 7, period = 3
• Still life (\(dx\) = \(dy\) = 0)
  • Integral sign: size = 6, period = 1

Using Z3 in the browser

Z3 comes with official TypeScript bindings and a WebAssembly build as the z3-solver package on npm. We originally used the Python Z3 API for the course project, but I found it straightforward to port the code to the TypeScript API. I wanted to write plain JavaScript and run the solver in the browser frontend, which required a couple extra steps:

• I used Browserify to bundle the bindings into JavaScript runnable in the browser.
• The z3-solver package requires threads, which means the environment needs SharedArrayBuffer support. This means the page has to be cross-origin isolated, but there's no way to set custom HTTP headers on GitHub Pages. Loading coi-serviceworker.js (the solution suggested by z3-solver's README) from this repo works—just make sure the script is in the same directory as the page.