{"cells":[{"metadata":{"_uuid":"8f2839f25d086af736a60e9eeb907d3b93b6e0e5","_cell_guid":"b1076dfc-b9ad-4769-8c92-a6c4dae69d19","trusted":true},"cell_type":"markdown","source":"# Reverse Game of Life - Z3 Constraint Satisfaction\n\n[Conway's Game of Life](https://en.wikipedia.org/wiki/Conway%27s_Game_of_Life) is an example of 2D cellular automata. \n\nI have previously written an interactive playable demo of the forward version of this game:\n- https://life.jamesmcguigan.com/\n\nUsing the classic ruleset on a 25x25 board with wraparound, the game evolves at each timestep according to the following rules\n- Overpopulation: if a living cell is surrounded by more than three living cells, it dies.\n- Stasis: if a living cell is surrounded by two or three living cells, it survives.\n- Underpopulation: if a living cell is surrounded by fewer than two living cells, it dies.\n- Reproduction: if a dead cell is surrounded by exactly three cells, it becomes a live cell.\n\nOr expressed algebraicly:\n- living + 4-8 neighbours = dies\n- living + 2-3 neighbours = lives\n- living + 0-1 neighbour  = dies\n- dead   +   3 neighbours = lives\n\n\nTo reverse the arrow of time:\n- any living cell must have had living 2-3 neighbours in the previous timestep\n- any dead cell must have had either 0-1 or 4-8 neighbours in the previous timestep\n- any dead cell with distance of greater than 2 from a living cell can be ignored and assumed to have 0 neighbours\n  - there are a near infinite number of self-contained patterns could have been born and died out in empty space\n  - however for the sake of the competition, ignoring them will greatly reduce the search space\n\n\nWhilst there have been many proposed solutions involving CNN neural networks (when all you have is a hammer, everything looks like a nail), this is in fact a classic constraint satisfaction problem. Here are some previous examples of using the Z3 library \n- https://www.kaggle.com/jamesmcguigan/z3-sudoku-solver\n- https://www.kaggle.com/jamesmcguigan/cryptarithmetic-solver"},{"metadata":{},"cell_type":"markdown","source":"# Z3 solver\n\nHere we define a Z3 solver, with a 3d (= 2d + time) grid of t_cells, representing the current board state and previous timesteps for the required delta to be solved.\n\nAs we are going backwards, we can ignore the rules for dead cells, and simply define the constraints required for the past timestep to produce living cells in the current timestep. We also define a rule to ignore any cells that currently have 0 neighbours to reduce the search space and prevent zero-point energy solutions.\n\nNOTE: With Z3 using boolean datatypes is 2-4x faster than using integer constraints"},{"metadata":{"trusted":true},"cell_type":"code","source":"# TODO: add z3-solver to kaggle-docker image\n! python3 -m pip install -q z3-solver\n! apt-get install -qq tree moreutils","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# Download git repository and copy to local directory\n!rm -rf /ai-games/\n!git clone https://github.com/JamesMcGuigan/ai-games/ /ai-games/\n# !cd /ai-games/; git checkout ad2f8cc94865f1be6083ca699d4b62b0cc039435\n!cp -rf /ai-games/puzzles/game_of_life/* ./   # copy code to kaggle notebook\n!rm -rf /kaggle/working/neural_networks/      # not relevant to this notebook\n!cd /ai-games/; git log -n1 ","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"Show the new filesystem contents of the notebook"},{"metadata":{"trusted":true},"cell_type":"code","source":"! pwd\n! tree -F","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Dataset Reimport Loop\n\nThere are 10 forks of this notebook running in parallel as a poor man's version of cluster compute using a modulo loop to subdivide the data, with the `submission.csv` file acting as a filesystem cache. They each reimport the output of each other, with the accumilated results of multiple 9-hour commit sessions merged together. \n\nEven still, this is a massive compute job and its going to take a while to finish all 50,000 entries in the test dataset given that each notebook can only compute a few hundred entries per commit cycle.\n\nWe also import any boards solved via the Hashmap Solver, which identifies geometric duplicates discovered from the training dataset, and generated data using forward play \n- https://www.kaggle.com/jamesmcguigan/game-of-life-hashmap-solver/"},{"metadata":{"trusted":true},"cell_type":"code","source":"# Merge submission files from various sources into a single file. Reverse sort puts non-zero entries first, then use awk to deduplicate on id\n!find ./ ../input/ /ai-games/puzzles/game_of_life/ -name 'submission.csv' | xargs cat | sort -nr | uniq | awk -F',' '!a[$1]++' | sort -n > ./submission_previous.csv\n!find ./ ../input/ /ai-games/puzzles/game_of_life/ -name 'submission.csv' | xargs cat | sort -nr | uniq | awk -F',' '!a[$1]++' | sort -n > ./submission.csv\n!find ./ ../input/ /ai-games/puzzles/game_of_life/ -name 'timeouts.csv'   | xargs cat | sort -nr | uniq | awk -F',' '!a[$1]++' | sort -n > ./timeouts.csv\n\n# Count number of non-zero entries in each submission.csv file\n!( for FILE in $(find ./ ../input/ /ai-games/puzzles/game_of_life/ -name '*submission.csv' | sort ); do cat $FILE | grep ',1' | wc -l | tr '\\n' ' '; echo $FILE; done) | sort -n;\n\n# BUGFIX: previous version of the code was computing to delta=-1, so replay submission.csv forward one step if required and validate we have the correct delta\n# This also generates stats\n!PYTHONPATH='.' python3 ./constraint_satisfaction/fix_submission.py","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Codebase\n\nFull codebase can be seen either in the output files section of the notebook or on my github repo:\n- https://github.com/JamesMcGuigan/ai-games/tree/master/puzzles/game_of_life"},{"metadata":{"trusted":true},"cell_type":"code","source":"%load_ext autoreload\n%autoreload 2\n\nimport itertools\nimport time\nimport numpy as np\nimport pandas as pd\nimport pydash\nfrom typing import Union, List, Tuple\nimport os\nimport sys\nfrom pathos.multiprocessing import ProcessPool\n\nfrom utils.plot import *\nfrom utils.game import *\nfrom utils.util import *\nfrom utils.datasets import *\nfrom utils.display_source import *\n\nprint('os.cpu_count()', os.cpu_count())\nnotebook_start = time.perf_counter()","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# These imports won't work inside Kaggle Submit without an internet connection to install Z3\nimport z3\nfrom constraint_satisfaction.z3_solver import *\nfrom constraint_satisfaction.solve_dataframe import *","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"This is the main codebase implementing the Z3 SAT Solver.\n\n- using Boolean rather than Integer logic results in a 2-4x speedup in solve times. \n- adding an additional constraint that any dead cell with zero neighbours should also be considered dead in the T=-1 timeframe dramatially reduces the state search space and prevents zero-point energy solutions (cells that are born and die in the vaccume of whitespace)"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./constraint_satisfaction/z3_solver.py')","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./constraint_satisfaction/z3_constraints.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"This is the main multiprocessing loop for processing submission.csv"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./constraint_satisfaction/solve_dataframe.py')","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./utils/idx_lookup.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"This is the forward implemention of the game of life implemented 3 different ways, with profiler measurements\n```\n  42.7µs - lambda: [ life_step(x)    for x in dataset ],  # 2882.0µs without numba\n 200.1µs - lambda: [ life_step_1(x)  for x in dataset ],\n  38.7µs - lambda: [ life_step_2(x)  for x in dataset ],\n```"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./utils/game.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"Casting functions for converting between datatypes"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./utils/util.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"This lets us plot out user-friendly visualiztions"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./utils/plot.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"Deployment specific lookups for the dataset .csv files "},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./utils/datasets.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"Test that all answers in the in the submission.csv file, when played forward, match the input data"},{"metadata":{"trusted":true},"cell_type":"code","source":"display_source('./test/test_submission.py')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Dataset"},{"metadata":{"trusted":true},"cell_type":"code","source":"test_df","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Range of Possible Solutions   \n\nHere we show the first 10 solutions to the first (very simple) datapoint, having excluded most of the zero-point energy solutions (ie clusters of cells that appear and dissapear in the vaccume of whitespace).\n\nTo find the exact starting conditions used by kaggle, would require computing valid solutions to T=-5 to account for the warmup period, but this can be very slow.\n\nNote how for even very simple starting conditions, there is a very large range of possible solutions"},{"metadata":{"trusted":true},"cell_type":"code","source":"idx      = 0  \ndelta    = csv_to_delta(train_df, idx)\nboard    = csv_to_numpy(train_df, idx, key='stop')\nexpected = csv_to_numpy(train_df, idx, key='start')\n\ntime_start     = time.perf_counter()\nsolution_count = 0\nz3_solver, t_cells, solution_3d = game_of_life_solver(board, delta, idx=idx)\nwhile np.count_nonzero(solution_3d):\n    solution_count += 1\n    plot_3d(solution_3d)\n    z3_solver, t_cells, solution_3d = game_of_life_next_solution(z3_solver, t_cells, verbose=True) # takes ~0.5s per solution\n    if solution_count > 5: break\n# print(f'Total Solutions: {solution_count} in {time.perf_counter() - time_start:.1f}s')  # too many to count","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Train Dataset"},{"metadata":{"trusted":true},"cell_type":"code","source":"idx      = 0\ndelta    = csv_to_delta(train_df, idx)\nboard    = csv_to_numpy(train_df, idx, key='stop')\nsolution_3d, idx, time_taken = solve_board_delta1_loop(board, delta, idx)\nplot_3d( solution_3d )","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Test Dataset\n\nAs we can see, large deltas are exponentially more difficult to solve than smaller deltas.\n\nWe can also use either joblib or pathos.multiprocessing to make full use of the 4 vCPU cores available in the Kaggle Kernel. \n\nThe modulo paramter lets me split training between kaggle notebooks and localhost compute whilst retaining sorting (lets solve the easy ones first). "},{"metadata":{"trusted":true},"cell_type":"code","source":"# test_df.loc[72539] | delta = 1 | time = 10.4s\n# test_df.loc[56795] | delta = 1 | time = 9.5s\n# test_df.loc[58109] | delta = 2 | time = 21.1s\n# test_df.loc[62386] | delta = 2 | time = 20.5s\n# test_df.loc[64934] | delta = 3 | time = 41.4s\n# test_df.loc[77908] | delta = 3 | time = 49.5s\n# test_df.loc[55567] | delta = 4 | time = 151.8s\n# test_df.loc[71076] | delta = 4 | time = 239.0s\n# test_df.loc[74622] | delta = 5 | time = 2119.0s\n# test_df.loc[75766] | delta = 5 | time = 1518.6s\n\nimport random\nfrom joblib import delayed\nfrom joblib import Parallel\nsubmision_df = pd.read_csv('submission.csv', index_col='id')  # manually copy/paste sample_submission.csv to location\n\njob_idxs = []\ndelta_batch_indexes = [0,10,100] \ndelta_idxs = {}\nfor delta in [1,2,3,4,5]:  # sorted(test_df['delta'].unique()):  # [1,2,3,4,5]\n    df   = test_df\n    df   = df[ df['delta'] == delta ]                                 # smaller deltas are exponentially easier\n    df   = df.iloc[ df.apply(np.count_nonzero, axis=1).argsort()  ]   # smaller grids are easiest \n    # idxs = get_unsolved_idxs(df, submision_df, modulo=(10,1) )      # don't recompute solved boards\n    idxs = list(df.index)                                             # show solved small boards\n    idxs = idxs[delta_batch_indexes]                                  # sample of small boards \n    delta_idxs[delta] = idxs\n    # quartiles from each delta - this takes far too long\n    # idxs = [ idxs[0], idxs[len(idxs)*1//4], idxs[len(idxs)*1//2], idxs[len(idxs)*3//4], idxs[-1] ] \n    job_idxs += idxs\nprint('delta_idxs', delta_idxs)\n    \njobs = []    \ndf   = test_df\nfor n, idx in enumerate(job_idxs):\n    delta = csv_to_delta(df, idx)\n    board = csv_to_numpy(df, idx, key='stop')\n    def job_fn(board, delta, idx):\n        time_start = time.perf_counter()\n        z3_solver, t_cells, solution_3d = game_of_life_solver(board, delta, idx=idx, verbose=True)\n        time_taken = time.perf_counter() - time_start\n        return solution_3d, idx, delta, time_taken \n    jobs.append( delayed(job_fn)(board, delta, idx) )\n        \n# jobs = []       \n# pathos.multiprocessing: Pool.uimap() is used for the submission.csv loop as it uses iterator rather than batch semantics  \njobs_output = Parallel(-2)(reversed(jobs))      # run longest jobs first \nfor solution_3d, idx, delta, time_taken in reversed(jobs_output):\n    print(f'test_df.loc[{idx}] | delta = {delta} | cells = {np.count_nonzero(solution_3d[-1])} | time = {time_taken:.1f}s')\n    if is_valid_solution_3d(solution_3d):        \n        plot_3d(solution_3d)\n        # Save to submission.csv.csv file         \n        submision_df          = pd.read_csv('submission.csv', index_col='id')\n        solution_dict         = numpy_to_dict(solution_3d[0])\n        submision_df.loc[idx] = pd.Series(solution_dict)\n        submision_df.sort_index().to_csv('submission.csv')\n    else:\n        print('Unsolveable!')\n        plot_idx(test_df, idx)","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Submission\n\nThere are 50,000 data points in the test dataset, which divided by the 9 hour notebook timeout gives us a performance requirement of 0.6s to solve each datapoint.\n\nFor performance optimiztion, `solve_dataframe()` uses pathos.multiprocessing, uses submission.csv as a cache file and persists after each solution is found, avoiding recomputing non-zero entries already in the file. Kaggle provides us with upto 10 * 9 hour commit sessions at once. `modulo % 10 == N` is used to evenly divide the dataset between 10 forked copies of itself, that can all be run simultaneously as the poor man's version of cluster compute. The notebooks then all reimport each other's output files and the multiple .csv files are merged in bash using `find|xargs|sort|awk`\n\nEven still, 50,000 entries is going to require a very large amount of compute, with notebooks being manually restarted every 9 hours. All I need to do is to [keep pushing the button](https://www.youtube.com/watch?v=xsksWR8uTDQ&ab_channel=busterroni11) without getting Lost."},{"metadata":{"trusted":true},"cell_type":"code","source":"notebook_time = (time.perf_counter() - notebook_start)\nprint(f'notebook_time = {notebook_time:.0f}s = {notebook_time/60:.1f}m')","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# submission_df = solve_dataframe(test_df, savefile='submission.csv', timeout=(7*60*60 - notebook_time), modulo=(1,0), max_timeout=3*60*60, plot=True)\n# submission_df = solve_dataframe(test_df, savefile='submission.csv', timeout=(0.1*60*60 - notebook_time), modulo=(9,1), plot=True)","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# Cleanup python caches to prevent poluting kaggle notebook outputs\n!find ./ -name '__pycache__' -or -name '*.py[cod]'  -delete","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Cluster Progress Counts\n\nAs a Count of [Sealand](https://en.wikipedia.org/wiki/Principality_of_Sealand), I do indeed [like to count](https://www.youtube.com/watch?v=ZIniljT5lJI), so this notbook has to end with a count of successfully solved games:"},{"metadata":{"trusted":true},"cell_type":"code","source":"# BUGFIX: previous version of the code was computing to delta=-1, so replay submission.csv forward one step if required and validate we have the correct delta\n# This also generates stats\n!PYTHONPATH='.' python3 ./constraint_satisfaction/fix_submission.py","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# Count number of non-zero entries in each submission.csv file\n!( for FILE in *.csv; do cat $FILE | grep ',1,' | wc -l | tr '\\n' ' '; echo $FILE; done ) | sort -n;","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Further Reading\n\nI have written an interactive playable demo of the forward version of this game in React Javascript:\n- https://life.jamesmcguigan.com/\n\n\nThis notebook is part of series exploring the Neural Network implementions of the Game of Life Foward Problem\n- [Pytorch Game of Life - First Attempt](https://www.kaggle.com/jamesmcguigan/pytorch-game-of-life-first-attempt)\n- [Pytorch Game of Life - Hardcoding Network Weights](https://www.kaggle.com/jamesmcguigan/pytorch-game-of-life-hardcoding-network-weights)\n- [Its Easy for Neural Networks To Learn Game of Life](https://www.kaggle.com/jamesmcguigan/its-easy-for-neural-networks-to-learn-game-of-life)\n\nThis is preliminary research towards the harder Reverse Game of Life problem, for which I have already designed a novel Ouroboros loss function: \n- [OuroborosLife - Function Reversal GAN](https://www.kaggle.com/jamesmcguigan/ouroboroslife-function-reversal-gan)\n\n\nI also have an extended series of Notebooks exploring different approaches to the Reverse Game of Life problem\n\nMy first attempt was to use the Z3 Constraint Satisfaction SAT solver. This gets 100% accuracy on most boards, but there are a few which it cannot solve. This approach can be slow for boards with large cell counts and large deltas. I managed to figure out how to get cluster compute working inside Kaggle Notebooks, but this solution is estimated to require 10,000+ hours of CPU time to complete.    \n- [Game of Life - Z3 Constraint Satisfaction](https://www.kaggle.com/jamesmcguigan/game-of-life-z3-constraint-satisfaction)\n\nSecond approach was to create a Geometrically Invarient Hash function using Summable Primes, then use forward play and a dictionary lookup table to create a database of known states. For known input/output states at a given delta, the problem is reduced to simply solving the geometric transform between inputs and applying the same function to the outputs. The Hashmap Solver was able to solve about 10% of the test dataset. \n- [Summable Primes](https://www.kaggle.com/jamesmcguigan/summable-primes)\n- [Geometric Invariant Hash Functions](https://www.kaggle.com/jamesmcguigan/geometric-invariant-hash-functions)\n- [Game of Life - Repeating Patterns](https://www.kaggle.com/jamesmcguigan/game-of-life-repeating-patterns)\n- [Game of Life - Hashmap Solver](https://www.kaggle.com/jamesmcguigan/game-of-life-hashmap-solver)\n- [Game of Life - Image Segmentation Solver](https://www.kaggle.com/jamesmcguigan/game-of-life-image-segmentation-solver)"}],"metadata":{"kernelspec":{"language":"python","display_name":"Python 3","name":"python3"},"language_info":{"pygments_lexer":"ipython3","nbconvert_exporter":"python","version":"3.6.4","file_extension":".py","codemirror_mode":{"name":"ipython","version":3},"name":"python","mimetype":"text/x-python"}},"nbformat":4,"nbformat_minor":4}