This post is loosely inspired by this mathoverflow post.

A Vanisher is any pattern in Conway's Game of life that completely disappears after one step. For example the following pattern is a size 9 Vanisher.

Size 9 Vanisher

An interesting property of Vanishers is that any pattern can be made into a vanishing one by simply adding more live cells. For example the following pattern can be completely enclosed into a vanishing pattern like so


However we can make that pattern into a Vanisher by adding even fewer live cells.

Smaller Enclosure Even Smaller Enclosure

Your task is to write a program that does this task for us. That is given a pattern as input find and output a vanishing pattern containing the input. You do not necessarily have to find the optimal pattern just a pattern that works.


To score your program you will have to run it on all of the size 6 polyplets (not double counting symmetrically equivalent cases). Here is a pastebin containing each polyplet on its own line. There should be 524 of them total. They are represented as a list of six coordinates ((x,y) tuples) each being the location of a live cell.

Your score will be the total number of new cells added to make all of these polyplets into Vanishers.


In the case of ties I will provide a list of the size 7 polyplets for the programs to be run on.


I would like IO to be pretty flexible you can take input and output in reasonable formats however you are probably going to want to take input in the same format as the raw input data I provided. Your format should be consistent across multiple runs.


Your program should run in a reasonable amount of time (approx <1 day) on a reasonable machine. I'm not going to really be enforcing this too much but I'd prefer if we would all play nice.

  • \$\begingroup\$ (of course you must be able to score your own code) \$\endgroup\$ – user202729 Jan 4 '18 at 16:31
  • \$\begingroup\$ Related meta for the last paragraph \$\endgroup\$ – user202729 Jan 4 '18 at 16:32
  • \$\begingroup\$ Are you going to ban hardcoding? \$\endgroup\$ – FlipTack Jan 4 '18 at 17:24
  • 1
    \$\begingroup\$ @FlipTack I'm pretty sure its already a standard loophole. Plus a well written program is probably just as good as a human anyway. \$\endgroup\$ – Post Rock Garf Hunter Jan 4 '18 at 17:25
  • 1
    \$\begingroup\$ @Οurous I think I'll just remove the third tie breaker. \$\endgroup\$ – Post Rock Garf Hunter Jan 5 '18 at 2:59

Python + Z3, score = 3647

Runs in 14 seconds on my eight core system.

from __future__ import print_function

import ast
import multiprocessing
import sys
import z3

def solve(line):
    line = ast.literal_eval(line)
    x0, x1 = min(x for x, y in line) - 2, max(x for x, y in line) + 3
    y0, y1 = min(y for x, y in line) - 2, max(y for x, y in line) + 3
    a = {(x, y): z3.Bool('a_{}_{}'.format(x, y)) for x in range(x0, x1) for y in range(y0, y1)}
    o = z3.Optimize()
    for x in range(x0 - 1, x1 + 1):
        for y in range(y0 - 1, y1 + 1):
            s = z3.Sum([
                z3.If(a[i, j], 1 + ((i, j) != (x, y)), 0)
                for i in (x - 1, x, x + 1) for j in (y - 1, y, y + 1) if (i, j) in a
            o.add(z3.Or(s < 5, s > 7))
    o.add(*(a[i, j] for i, j in line))
    o.minimize(z3.Sum([z3.If(b, 1, 0) for b in a.values()]))
    assert o.check() == z3.sat
    m = o.model()
    return line, {k for k in a if z3.is_true(m[a[k]])}

total = 0
for line, cells in multiprocessing.Pool().map(solve, sys.stdin):
    added = len(cells) - len(line)
    print(line, added)
    x0, x1 = min(x for x, y in cells), max(x for x, y in cells) + 1
    y0, y1 = min(y for x, y in cells), max(y for x, y in cells) + 1
    for y in range(y0, y1):
        print(''.join('#' if (x, y) in line else '+' if (x, y) in cells else ' ' for x in range(x0, x1)))
    total += added
print('Total:', total)

Full output

  • 1
    \$\begingroup\$ A decent explanation of how this works would be good and would win my upvote. It seems it tries a brute force of adding cells to a rectangular area surrounding the polyplet? \$\endgroup\$ – Level River St Jan 5 '18 at 3:35
  • \$\begingroup\$ It was unclear to me why there are + disconnected from the main shape in some cases but it seems they are necessary to avoid spawning new cells. Are these solutions therefore optimal? \$\endgroup\$ – Level River St Jan 5 '18 at 3:36
  • \$\begingroup\$ Out of curiosity, why use z3.Or instead of vanilla a or b? Is it purely performance, or does it have a different functionality? \$\endgroup\$ – caird coinheringaahing Jan 5 '18 at 4:24
  • \$\begingroup\$ @cairdcoinheringaahing Looks like that's a symbolic solution. \$\endgroup\$ – user202729 Jan 5 '18 at 5:29
  • 1
    \$\begingroup\$ @AndersKaseorg 1. you haven't answered my comment asking if your solutions are optimal. This is of great importance to anyone else considering posting an answer. 2. If you don't explain what Z3 does in your answer I can only guess what it does, as I don't have time to read the documentation, hence my random guess of brute force. 3 This answer deserves an upvote (in fact it deserves many upvotes) for its code, but I won't upvote until an explanation covering the above two points is added to the answer. \$\endgroup\$ – Level River St Jan 6 '18 at 0:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.