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.

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.

Post Rock Garf Hunter

Posted 2018-01-04T16:24:00.890

Reputation: 55 382

(of course you must be able to score your own code) – user202729 – 2018-01-04T16:31:13.997

Related meta for the last paragraph – user202729 – 2018-01-04T16:32:06.753

Are you going to ban hardcoding? – FlipTack – 2018-01-04T17:24:07.793

1@FlipTack I'm pretty sure its already a standard loophole. Plus a well written program is probably just as good as a human anyway. – Post Rock Garf Hunter – 2018-01-04T17:25:07.500

Is this a [tag:test-battery]? – H.PWiz – 2018-01-04T18:00:06.540

@H.PWiz Looks like it is. For some reason I had a different idea of what [tag:test-battery] was. – Post Rock Garf Hunter – 2018-01-04T18:05:22.473

the first person to successfully score their program [...] will be the winner [tag:fastest-scoring]? – Erik the Outgolfer – 2018-01-04T19:37:33.283

@EriktheOutgolfer I guess? It's the second tie breaker so I don't really anticipate having to break that out. – Post Rock Garf Hunter – 2018-01-04T19:38:41.567

"well written program is probably just as good as a human"... or even better... depends on the objective. Also... @WheatWizard The format of the test cases are a list of a (row, column) tuple, correct? – user202729 – 2018-01-05T00:58:15.193

@user202729 Yes, I'll make that clear in the question. Although it doesn't matter if it's row,column or column,row because of symmetry. – Post Rock Garf Hunter – 2018-01-05T01:16:45.760

Just to clarify, it has to work for any size of polyplets? – Οurous – 2018-01-05T02:18:58.790

@Οurous In theory it should work for any input pattern. You are free to optimize for polyplets though. – Post Rock Garf Hunter – 2018-01-05T02:29:19.127

Would it not make more sense to have the tie break be runtime speed? Since people have different time-zones, the fastest posted scoring could disadvantage some people by many hours, simply because they're sleeping or at work. – Οurous – 2018-01-05T02:55:34.413

1@Οurous I think I'll just remove the third tie breaker. – Post Rock Garf Hunter – 2018-01-05T02:59:19.007



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

Anders Kaseorg

Posted 2018-01-04T16:24:00.890

Reputation: 29 242

1A 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? – Level River St – 2018-01-05T03:35:10.527

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 – 2018-01-05T03:36:51.910

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 – 2018-01-05T04:24:50.273

@cairdcoinheringaahing Looks like that's a symbolic solution. – user202729 – 2018-01-05T05:29:09.970

@LevelRiverSt Z3 is a constraint solver from Microsoft Research that’s much more intelligent than brute force. All that’s happening is this code is declaring the constraints to hand to Z3. We tell Z3 that every cell in some rectangle might be alive or dead, add constraints saying that the next frame is entirely dead, add constraints saying that the given cells are currently alive, and ask it to minimize the number of live cells. All the real work happens in Z3 inside o.check(). – Anders Kaseorg – 2018-01-05T08:10:28.670

@cairdcoinheringaahing s < 5 is a constraint, not a boolean, so the Python or operator cannot be used. (Operators like < are overloaded to work on Z3 symbolic expressions, but or cannot be overloaded.) – Anders Kaseorg – 2018-01-05T08:14:03.097

1@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. – Level River St – 2018-01-06T00:18:52.770

@LevelRiverSt "What Z3 does"... "constraint solver", that's it. How it solves the constraints and whether it's optimal is implementation-defined. Although, a link to documentation would be useful. – user202729 – 2018-01-06T07:14:05.553

@user202729 The main thing is whether the constraint solver ifinds optimal solutions or not, and "yes / no / don't know if if it finds optimal solutions" is something the OP should be able to answer and would be best included the post as it is relevant to scoring. That's my main issue. That said, additional details of what OP's code does and what the Z3 functions do would also also enhance the post. I hate having to squint through code to work out what it does when it contains an import from an unfamiliar library. – Level River St – 2018-01-06T07:31:33.933

The problem arises because the constraint solver has clearly done an excellent job and many of the solutions are clearly optimal! Whether they are in theory all optimal / in practice all optimal is another thing. – Level River St – 2018-01-06T07:43:11.003

@LevelRiverSt Any failure of Z3 to find the optimal solution like we asked for would be a bug in Z3. I am amused that you think you can control my writing style by holding upvotes hostage. Any post will have some readers who are familiar with the language and libraries and some readers who aren’t (I don’t think every Retina answer should feel obligated to explain what regular expressions are). Although Z3 is kind of a big deal in the world of constraint solvers, it’s fine if you personally haven’t heard of it. You’re welcome to follow the link I already provided or Google for more information. – Anders Kaseorg – 2018-01-06T22:46:40.253

(That said, I haven’t attempted to prove that extending the rectangle by two cells is sufficient to encompass the optimal solution, although it empirically seems to be sufficient.) – Anders Kaseorg – 2018-01-06T22:48:23.937

@AndersKaseorg Any failure to find the optimal solution...would be a bug in Z3 This cannot be deduced from your post by someone unfamiliar with Z3 as indicated by user202729. Thank you for answering my question, I am now upvoting, though I would suggest you include your comments in the post as it would make it easier for others unfamiliar with Z3 to appreciate it. – Level River St – 2018-01-07T02:37:55.047

As for holding upvotes hostage... I'm free to vote as I please and you to write as you please. I usually comment when I downvote - It's a common complaint that people don't leave reasons for downvotes. Here I merely chose to express the conditions under which I would upvote (and from by the upvote on my comment, someone else has a similar view.) I like your post a lot and spent some time trying to understand it. I find it odd that you would seek to restrict your audience to those familiar with Z3 or inclined to read its documention when it would be simple to explain briefly, but your choice. – Level River St – 2018-01-07T02:53:43.490