[jfries]

Since propagation of information is limited to one cell per step, it's possible to speed this up by splitting the image into smaller subimages and solving those first, and then solve the borders between such subimages.

This technique can be used to solve multiple steps as well, the only change is that the border between subimages becomes thicker.

[OscarCunningham]

I wouldn't expect this to produce a speedup, because the SAT solver will already be doing it!

[newswasboring]

Yeah but for a sufficiently big image I think segregation will help if we do some sort of memoization. But I guess SAT solvers may be doing that too internally.

[OscarCunningham]

That's a good point. Life has translation symmetry that the SAT solver can't see. So if copies of the same region appear in your pattern more than once then you could plausibly save the SAT solver time by telling it to use the same predecessor for all of them.

[remcob]

You can see this in the flower image. The target image has a lot of symmetries (reflections, rotations) that also exist in the GoL ruleset. So must be a parent that also has these symmetries. Yet the found solution has none of these symmetries.

[OscarCunningham]

Consider the 3×3 block of live cells:

    .....
    .ooo.
    .ooo.
    .ooo.
    .....

It has no parent with the same symmetry, since every neighbour of the centre cell would be the same but a cell can't live or be born with 0 or 4 neighbours.

But it does have a parent with less symmetry:

    .....
    .....
    ooooo
    .....
    .....

[remcob]

True, and this is a counterexample to my claim that the parent would retain the symmetry. I think it can be refined though:

The parent still has hor/ver mirror symmetries, and the solution rotated is also a solution. So there is a set of (in this case two) parents that is invariant under the same symmetries.

In general, a parent should still be a parent when any of the targets symmetries are applied. (But it wouldn't necessarily be the same parent).

This can be captured in a SAT by insisting that any symmetry of a solution is also a solution, which adds a lot of new constraints and no new variables, so should help with finding.