试玩 Z3……速度好慢，搜个 25P3H1V0.1 都要十几秒。懒得支持生命游戏以外的规则以及对称性了。

z3_life_search.py

#!/usr/bin/env python

from z3 import *
import sys

class LifeSearch:
    nbhd = {(i, j): 1 if i == j == 0 else 2
            for i in range(-1,2)
            for j in range(-1,2)}

    def __init__(self, x, y, p = 1, dx = 0, dy = 0):
        self.x = x
        self.y = y
        self.p = p
        self.dx = dx
        self.dy = dy

    def __getitem__(self, ix):
        t = 0 if len(ix) < 3 else ix[2]
        i = ix[0] - self.dx * (t // self.p)
        j = ix[1] - self.dy * (t // self.p)
        t = t % self.p
        if 0 <= i < self.x and 0 <= j < self.y:
            return Bool(f"c_{i}_{j}_{t}")
        else:
            return BoolVal(False)

    def get_nbhd(self, i, j, t):
        return [(self[i + d[0], j + d[1], t], w) for d, w in self.nbhd.items()]

    def cell_constraint(self, i, j, t):
        return self[i, j, t + 1] == And(PbGe(self.get_nbhd(i, j, t), 5),
                                        PbLe(self.get_nbhd(i, j, t), 7))

    def solve(self):
        s = SolverFor("QF_FD")
        
        for i in range(-1, self.x + 1):
            for j in range(-1, self.y + 1):
                for t in range(self.p):
                    s.add(self.cell_constraint(i, j, t))

        s.add(Or([self[i,j] if self.p == 1 else self[i,j,0] != self[i,j,1] 
                  for i in range(self.x)
                  for j in range(self.y)]))

        if s.check() == unsat:
            return 'no solution'

        m = s.model()

        r = ""
        for i in range(self.x):
            for j in range(self.y):
                r += 'o' if m[self[i,j]] else '.'
            r += '\n'

        return r

print(LifeSearch(*list(map(int,sys.argv[1:6]))).solve())