A SAT forward solver for John Conway's "Game of Life" based on z3.
You will need Python 3. Initialize virtual environment and install the dependencies:
virtualenv venv --python=/usr/bin/python3
venv/bin/activate
pip3 install -r requirements.txtThen try to run the solver on the examples:
python3 solver.py examples/field1.txt
python3 solver.py examples/field2.txtThe first line describes field settings in the following format: <width> <height> <number of transitions>.
Subsequent lines describe the field where:
.is a dead cell*is an alive cell
- TAOCP 4A describes the basic idea behind solving of the Game of Life in chapter 7.2.2.2.
- flopp/gol-sat – the implementation of the similar solver using C++ and MiniSAT