Strategic Vanishers

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.

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.

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.

Scoring

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.

Ties

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

IO

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.

Timing

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.

• (of course you must be able to score your own code) – user202729 Jan 4 '18 at 16:31
• Related meta for the last paragraph – user202729 Jan 4 '18 at 16:32
• Are you going to ban hardcoding? – FlipTack Jan 4 '18 at 17:24
• @FlipTack I'm pretty sure its already a standard loophole. Plus a well written program is probably just as good as a human anyway. – Sriotchilism O'Zaic Jan 4 '18 at 17:25
• @Οurous I think I'll just remove the third tie breaker. – Sriotchilism O'Zaic 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):
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)))

• 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? – Level River St Jan 5 '18 at 3:36
• Out of curiosity, why use z3.Or instead of vanilla a or b? Is it purely performance, or does it have a different functionality? – caird coinheringaahing Jan 5 '18 at 4:24