SAT搜索发现“罗宾爵士”，康威生命游戏48年来首个基本骑士飞船

48年来，康威生命游戏中已知的基本飞船要么直线移动，要么对角线移动。斜向飞船确实存在，但只是像Waterbear那样由滑翔机和电路构成的庞大工程结构，而非紧凑的基本图案。一些尝试过搜索的玩家甚至怀疑基本斜向飞船根本不存在。

暴力破解毫无希望，更聪明的遗传搜索同样不行。几乎每个随机配置在生命游戏中都会消亡，演化对初始条件极其敏感，绝大多数搜索空间的适应度为零，没有梯度可供遗传算法攀登。

发现者转而将问题变成可满足性问题。他的MetaSAT项目中的程序ikpx，将寻找斜向滑翔机编码为一组SAT约束：生命游戏规则，图案每六代横向移动两格纵向移动一格的位移要求，该斜率下经证明的最小周期，以及搜索区域的边界。启发式约束，例如搜索长薄型飞船而非任意形状，大大缩减了搜索空间，ikpx将整个约束条件交给现代化SAT求解器。

求解器返回“罗宾爵士”，在生命游戏维基上被编录为282P6H2V1：首个基本斜向滑翔机，也是48年来首个新斜率的基本飞船，以该斜率最大的可能速度移动。代码公开发布后，社区成员已报告建成了反应器和探测器，而这一发现在Hacker News上获得了733分和143条评论。

不要暴力破解或演化图案；将“存在这样一个位移的飞船”编码为SAT约束，让求解器搜索

将“寻找图案”编码为可满足性问题，把搜索交给SAT求解器，而数十年的研究已让这些求解器强大得惊人。

诸如长薄型而非任意形状的启发式约束，在不排除目标类别的情况下剔除绝大多数候选空间。

针对(2,1)位移及其经证明的六代最小周期，意味着搜索瞄准最快可能斜向飞船，所以首次成功一举终结了48年的疑问。

暴力与遗传搜索没有进展，因为几乎每个生命图案都会消亡，且微小变化会引起连锁反应，而约束搜索不需要适应度梯度。

结果是基本且紧凑的，足够用作构建模块，开放的代码和交互式查看器让社区得以验证并加以利用。

当搜索空间没有梯度且几乎无幸存者时，不要盲目采样：将存在性编码为约束，用领域启发式缩减空间，让求解器去探索

罗宾爵士于2018年3月6日在康威生命游戏论坛上公布，3月8日发到Hacker News，获得733分和143条评论；评论者引用论坛称这是48年来第一个新斜率的基本飞船，并指出它出现在几乎骑士船之后14年。生命游戏维基将其编录为282P6H2V1，有社区成员报告已建成反应器和探测器。此外，用枪机或滑翔机合成的方法被认为可能要难上几个数量级。发现该图案的ikpx与MetaSAT代码已发布在GitLab上。