{"cells":[{"metadata":{},"cell_type":"markdown","source":"# Perfect Solve of Puzzles using a SAT solver\n\nKaggle's [Conway's Reverse Game of Life 2020](https://www.kaggle.com/c/conways-reverse-game-of-life-2020/overview) can be viewed as a [boolean satisfiability problem](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem).\n\nIn this notebook, we will:\n - presents the problem in a form solvable by SAT solver\n - use in a notebook the [kissat SAT solver](http://fmv.jku.at/kissat/), which won first place in the main track of the [SAT Competition 2020](https://satcompetition.github.io/2020) and first place on unsatisfiable instances.\n"},{"metadata":{"trusted":true},"cell_type":"code","source":"import os\nimport random\nimport subprocess\nimport time\n\nimport numpy as np\nimport pandas as pd\n\nfrom joblib import Parallel, delayed\nfrom scipy.signal import convolve2d\nfrom sklearn.metrics import mean_absolute_error\nfrom sympy.logic import POSform","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"TIME_BUDGET = 8.9 * 3600  # Maximum time allowed for our notebook\nMAX_BUDGET = 10  # Maximum time spent on a single puzzle\nN = 25  # grid dimension\nDELTAS=(1, )  # list of deltas we are trying to solve","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Install and compile kissat SAT solver from sources"},{"metadata":{"trusted":true},"cell_type":"code","source":"!git clone https://github.com/arminbiere/kissat.git >/dev/null\n!cd kissat && ./configure && make all >/dev/null","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Generate CNF for one cell (live or dead)\n\nTo use a SAT solver we must express the problem in the [conjunctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form) (CNF).\n\nThe easiest way I found to generate the proble in CNF, is to create the truth table of the problem and use the [Quine–McCluskey algorithm](https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm) to generate an optimal CNF.\n\nWe are lucky `sympy` implements it.\n\n\nFollowing code will generate all cases of a 3x3 grid on which we apply the Game Of Life rules. Two lists keep results of combinations resulting in `live` or `dead`  cell. Each cell of the 3x3 grid is represented by a letter `a` to `i`:"},{"metadata":{"scrolled":false,"trusted":true},"cell_type":"code","source":"# a b c\n# d e f\n# g h i\n\nlive = []\ndead = []\nfor a in (0,1):\n    for b in (0,1):\n        for c in (0,1):\n            for d in (0,1):\n                for e in (0,1):\n                    for f in (0,1):\n                        for g in (0,1):\n                            for h in (0,1):\n                                for i in (0,1):\n                                    crown = (a+b+c+d+ f+g+h+i)\n                                    var = [a, b, c, d, e, f, g, h, i]\n                                    if crown == 3 or (e == 1 and crown == 2):\n                                        live.append(var)\n                                    else:\n                                        dead.append(var)\n\nlive = POSform(['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i'], live)\ndead = POSform(['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i'], dead)","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"Here is the CNF that a live cell shall validate:"},{"metadata":{"scrolled":false,"trusted":true},"cell_type":"code","source":"live","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### CNF for the general case\n\n`x` is the resulting cell."},{"metadata":{"trusted":true},"cell_type":"code","source":"# x\n\n# a b c\n# d e f\n# g h i\n\nvalid = []\nfor a in (0,1):\n    for b in (0,1):\n        for c in (0,1):\n            for d in (0,1):\n                for e in (0,1):\n                    for f in (0,1):\n                        for g in (0,1):\n                            for h in (0,1):\n                                for i in (0,1):\n                                    crown = (a+b+c+d+ f+g+h+i)\n                                    x = 1 if crown == 3 or (e == 1 and crown == 2) else 0\n                                    var = [x, a, b, c, d, e, f, g, h, i]\n                                    valid.append(var)\n\nvalid = POSform(['x', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i'], valid)","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Compute score of each puzzle"},{"metadata":{"trusted":true},"cell_type":"code","source":"def life_step(X):\n    nbrs_count = convolve2d(X, np.ones((3, 3)), mode='same', boundary='wrap') - X\n    return (nbrs_count == 3) | (X & (nbrs_count == 2))\n\n\ndef individual_scores(pred):\n    scores = []\n    for i in df.index:\n        delta = df.loc[i][0]\n        start = np.asarray(pred.loc[i]).reshape(N, N)\n        end   = np.asarray(df.loc[i][1:]).reshape(N, N)\n        x = start\n        for _ in range(delta):\n            x = life_step(x)\n        scores.append(mean_absolute_error(x, end))\n    return scores","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Turn into a template"},{"metadata":{"scrolled":false,"trusted":true},"cell_type":"code","source":"def templatize(cnf):\n    return (\n        str(cnf)\n        .replace(' & ', ' 0\\n')\n        .replace(' | ', ' ')\n        .replace('(', '')\n        .replace(')', '')\n        .replace('~', '-')\n        + ' 0\\n'\n    )","execution_count":null,"outputs":[]},{"metadata":{"scrolled":false,"trusted":true},"cell_type":"code","source":"template_live = templatize(live)\ntemplate_dead = templatize(dead)\ntemplate_intermediate = templatize(valid)","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"def replace(template, a, b, c, d, e, f, g, h, i, x=None):\n    return (\n        template\n        .replace('a', str(a))\n        .replace('b', str(b))\n        .replace('c', str(c))\n        .replace('d', str(d))\n        .replace('e', str(e))\n        .replace('f', str(f))\n        .replace('g', str(g))\n        .replace('h', str(h))\n        .replace('i', str(i))\n        .replace('x', str(x))\n    )","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"def wrap(val):\n    return (val + N) % N","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"# convert a position (x, y) at layed d to a variable number\ndef v(x, y, d):\n    return 1 + wrap(x) + wrap(y) * N + d * N * N","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"def get_clauses(puzzle, delta):\n    clauses = ''\n    \n    for x in range(N):\n        for y in range(N):\n\n            clauses += replace(template_live if puzzle[x, y] else template_dead,\n                            v(x-1, y-1, 0), v(x, y-1, 0), v(x+1, y-1, 0),\n                            v(x-1, y  , 0), v(x, y  , 0), v(x+1, y  , 0),\n                            v(x-1, y+1, 0), v(x, y+1, 0), v(x+1, y+1, 0))\n\n    for d in range(1, delta):\n        for x in range(N):\n            for y in range(N):\n                clauses += replace(template_intermediate,\n                                v(x-1, y-1, d), v(x, y-1, d), v(x+1, y-1, d),\n                                v(x-1, y  , d), v(x, y  , d), v(x+1, y  , d),\n                                v(x-1, y+1, d), v(x, y+1, d), v(x+1, y+1, d),\n                                v(x, y, d-1))\n    return clauses","execution_count":null,"outputs":[]},{"metadata":{"trusted":true},"cell_type":"code","source":"def error(idx, pred):\n    delta = df.loc[idx][0]\n    end = np.asarray(df.loc[idx][1:]).reshape(N, N)\n\n    x = pred\n    for _ in range(delta):\n        x = life_step(x)\n\n    return mean_absolute_error(x, end)","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Solve one puzzle"},{"metadata":{"trusted":true},"cell_type":"code","source":"def solve(idx):\n    budget = TIME_BUDGET - (time.time() - start_time)\n    budget = min(budget, MAX_BUDGET)\n    if budget <= 0:\n        return None\n    \n    # load puzzle\n    delta = df.loc[idx][0]\n    puzzle = np.asarray(df.loc[idx][1:]).reshape(N,N)\n\n    # get SAT clauses\n    clauses = get_clauses(puzzle, delta)\n    nb = clauses.count('\\n')\n\n    # write .cnf file\n    filename = f'puzzles_cnf/{idx}.cnf'\n    with open(filename, 'w') as f:\n        f.write(f'c puzzle {idx}, delta {delta}\\n')\n        f.write(f'p cnf {N*N*delta} {nb}\\n')\n        f.write(clauses)\n    \n    # invoke kissat\n    cmd = [\"timeout\", f'{budget}s', \"./kissat/build/kissat\", \"-q\", filename]\n    cmd = subprocess.Popen(cmd, stdout=subprocess.PIPE)\n    solution = cmd.communicate()[0]\n    solution = solution.decode('utf8')\n    os.remove(filename)\n    \n    if solution == '':\n        print(idx, \"timeout\")\n        return None\n        \n    print(idx, \"solved\")\n\n    # parse solution\n    parsed = []\n    for x in solution.split():\n        try:\n            parsed.append(int(x))\n        except:\n            pass\n    parsed = set(parsed)\n\n    # format solution\n    solution = np.zeros((N, N), dtype=int)\n    for x in range(N):\n        for y in range(N):\n            z = v(x, y, delta-1)\n            if z in parsed:\n                solution[x, y] = 1\n\n    return solution","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Load puzzles"},{"metadata":{"trusted":true},"cell_type":"code","source":"df = pd.read_csv('../input/conways-reverse-game-of-life-2020/test.csv', index_col='id')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Use test.csv as baseline of our submission"},{"metadata":{"trusted":true},"cell_type":"code","source":"!mkdir -p puzzles_cnf\nsubmission = df.copy()\nsubmission.drop(['delta'], inplace=True, axis=1)\nsubmission['score'] = individual_scores(submission)","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Order puzzles to solve easy ones first"},{"metadata":{"trusted":true},"cell_type":"code","source":"to_solve = list(set(df[df.delta.isin(DELTAS)].index).intersection(set(submission[submission.score > 0].index)))\nto_solve = [x for _, x in sorted(zip(submission.loc[to_solve].score / df.loc[to_solve].delta, to_solve), reverse=True)]","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Run Jobs in Parallel"},{"metadata":{"scrolled":false,"trusted":true},"cell_type":"code","source":"start_time = time.time()\n\nsolutions = Parallel(n_jobs=-1)(\n    delayed(solve)(i) for i in to_solve\n)\n\nprint(f'Completely solved {sum([x is not None for x in solutions])} puzzles in {time.time() - start_time:.2f} seconds 🔥🔥🔥')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"### Save submission"},{"metadata":{"trusted":true},"cell_type":"code","source":"submission.drop(['score'], axis=1, inplace=True)\n\nfor i, s in zip(to_solve, solutions):\n    if s is not None:\n        submission.loc[i] = s.reshape(N*N)\n\nsubmission.rename(columns={f'stop_{x}': f'start_{x}' for x in range(N*N)}, inplace=True)\nsubmission.to_csv(f'submission.csv')","execution_count":null,"outputs":[]},{"metadata":{},"cell_type":"markdown","source":"# Conclusion\n\nThis approach helped to solve all puzzles with `delta` equal to 1 or 2.\n\nI learnt a lot about SAT and CNF during this competition.\n\nIf you like this notebook, please leave a comment 🖊, upvote 👍, and put a smile on your face 😀."}],"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}