Strategic Vanishers

Question

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.

Answer 1

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