我在这次比赛中的方法是尝试多种不同的技术，并在整个比赛过程中公开发表我所有正在进行的研究，这导致我在排行榜后面留下了一小串“公共笔记本集成”的追随者。

结果

交互式可玩游戏

我之前用 React Javascript 写了一个正向版本游戏的交互式演示：

• https://life.jamesmcguigan.com/

Z3 约束满足

• https://www.kaggle.com/jamesmcguigan/game-of-life-z3-constraint-satisfaction

我的第一次尝试是使用 Z3 SAT 求解器。

在设计上，这是通过一个回溯 delta 步数的 3D 单元格网格来实现的。生命游戏的正向规则被添加为约束，连同停止棋盘位置和一个非空棋盘约束。

作为性能优化，添加了一个额外的约束，即任何没有邻居的死单元在前一个时间步也是死的。这有助于防止在空白区域出现无限数量的“零点能”解（即细胞在空白中凭空出现和消失）。然而，这导致少数需要距离为 2 空白的棋盘出现不可满足（unsat）。Z3 的 push 和 pop 用于检查 distance=1 约束，然后在 unsat 时将其替换为 distance=2。

我还发现，使用布尔逻辑而不是整数逻辑带来了 2-4 倍的性能提升。

这种方法的主要限制是 CPU 运行时间。较大的 delta 和高细胞计数（空白较少）将呈指数级增长耗时。即使使用 pathos 多进程利用所有 4 个 CPU，仍然需要 20,000 小时的 CPU 运行时间才能达到 0.08410 的分数 = 29,121/50,000 = 58%。