SAT探索により、コンウェイのライフゲームで48年ぶりの初の基本的斜行宇宙船「サー・ロビン」が発見される

48年間、コンウェイのライフゲームで知られていたすべての基本的宇宙船は、直交方向か対角方向のいずれかに移動するものだった。斜行宇宙船は存在していたが、ウォーターベアのようにグライダーと回路から組み立てられた巨大な人工構造物としてのみであり、コンパクトな基本パターンとしては存在しなかった。探索を試みたプレイヤーの中には、基本的な斜行宇宙船がそもそも存在するのか疑う者もいた。

総当たり探索は絶望的であり、明らかに賢いアイデアである遺伝的探索も同様だった。ライフゲームではほぼすべてのランダムな配置が死滅し、進化は初期条件に極めて敏感で、探索空間の圧倒的大部分は適合度がゼロであり、遺伝的アルゴリズムが登るべき勾配が存在しなかった。

発見者は代わりにこれを充足可能性問題にした。彼のMetaSATプロジェクトの一部であるikpxというプログラムは、斜行グライダーの発見を一連のSAT制約として定式化した。すなわち、ライフゲームの遷移規則、パターンが6世代ごとに水平方向に2セル、垂直方向に1セル変位するという要件、その傾きについて証明された最小周期、そして探索領域の境界である。長く薄い宇宙船を探索する（任意の形状ではなく）といったヒューリスティックな制約によって空間が削減され、ikpxは結果として得られた制約の塊を現代的なSATソルバーに渡した。

ソルバーはサー・ロビンを返した。ライフウィキでは282P6H2V1として登録されており、最初の基本的斜行グライダーであり、48年ぶりに新しい傾きを持つ最初の基本的宇宙船であり、その傾きで可能な最大速度で移動する。コードは公開され、コミュニティのメンバーはイーターと検出器がすでに構築されたと報告し、この発見はHacker Newsで733ポイントと143件のコメントを集めた。

パターンを総当たり探索したり進化させたりするのではなく、「この変位を持つ宇宙船が存在する」ことをSAT制約として符号化し、ソルバーに探索させること

「パターンを見つける」ことを充足可能性として符号化することで、数十年の研究によって驚くほど強力になったSATソルバーに探索を委ねることができる。

任意の形状ではなく長く薄いといったヒューリスティックな制約は、対象クラスを排除することなく、候補空間の圧倒的大部分を除去する。

証明された6世代という最小周期を持つ(2,1)変位を狙うことで、探索は可能な限り最速の斜行宇宙船を目指すことになり、最初の成功が48年来の問いに決着をつけた。

ライフゲームのパターンはほとんどが死滅し、小さな変化が連鎖するため、総当たり探索や遺伝的探索には手がかりがなかったが、制約探索には適合度の勾配が不要である。

結果は基本的かつコンパクトで、有用な構成要素となり得るものであり、公開されたコードとインタラクティブなビューアによってコミュニティが検証し、発展させることができた。

探索空間に勾配がなく、生存者がほとんどいない場合、盲目的にサンプリングするのではなく、存在を制約として符号化し、ドメインのヒューリスティックで空間を削減し、探索をソルバーに任せること

サー・ロビンは2018年3月6日にコンウェイのライフゲームのフォーラムで発表され、3月8日にHacker Newsに投稿されて733ポイントと143件のコメントを集めた。コメント投稿者たちはフォーラムの「48年ぶりに新しい傾きを持つ最初の基本的宇宙船」という表現を引用し、それがほぼナイトシップの14年後にもたらされたことに言及した。ライフウィキはこれを282P6H2V1として登録し、コミュニティのメンバーはイーターと検出器がすでに構築されたと報告し、ナイトシップのガンやグライダー合成は桁違いに難しいと判断された。パターンを発見したikpxとMetaSATのコードはGitLabで公開された。