SAT 搜尋找到 Sir Robin，康威生命遊戲 48 年來首個基本斜向飛船

48 年來，康威生命遊戲中已知的每一個基本飛船，移動方向不是正交就是對角。斜向飛船確實存在，但僅限於由滑翔機與電路組裝而成的大型工程結構，例如 Waterbear，而非緊湊的基本圖樣。一些曾嘗試搜尋的玩家甚至懷疑基本斜向飛船根本不存在。

暴力搜尋毫無希望，而顯而易見的聰明想法也一樣：遺傳搜尋。生命遊戲中幾乎每一個隨機組態都會消亡，演化對初始條件極度敏感，而且絕大多數搜尋空間的適應度為零，沒有梯度可供遺傳演算法攀升。

發現者改而把它變成可滿足性問題。名為 ikpx 的程式屬於他的 MetaSAT 專案，將尋找斜向滑翔機表述為一組 SAT 約束：生命遊戲的轉移規則、圖樣每六代水平位移兩格且垂直位移一格的要求、該斜率已證明的最小週期，以及搜尋區域的邊界。啟發式約束（例如搜尋細長飛船而非任意形狀）縮小了空間，ikpx 再將這團約束交給現代 SAT 求解器。

求解器回傳了 Sir Robin，在 Life Wiki 上編目為 282P6H2V1：這是首個基本斜向滑翔機，也是 48 年來首個具有新斜率的基本飛船，以該斜率可能達到的最高速度移動。程式碼已公開，社群成員回報已建好 eater 與偵測器，這項發現也在 Hacker News 上獲得 733 分與 143 則留言。

不要暴力搜尋或演化圖樣；把「存在具有此位移的飛船」編碼為 SAT 約束，讓求解器去搜尋

把「尋找圖樣」編碼為可滿足性問題，將搜尋交給 SAT 求解器，數十年的研究已讓它們出奇強大。

諸如細長而非任意形狀的啟發式約束，排除了絕大多數候選空間，卻不排除目標類別。

鎖定 (2,1) 位移及其已證明的六代最小週期，意味著搜尋瞄準了可能最快的斜向飛船，因此首次成功便徹底解決了 48 年的問題。

暴力搜尋與遺傳搜尋都無從著力，因為幾乎每個生命圖樣都會消亡、微小改變會連鎖放大，而約束搜尋不需要適應度梯度。

結果既基本又緊湊，足以作為有用的積木，而公開的程式碼與互動式檢視器讓社群得以驗證並在其上繼續建構。

當搜尋空間沒有梯度且幾乎沒有存活者時，不要盲目取樣：把存在性編碼為約束，用領域啟發式縮小空間，讓求解器去探索

Sir Robin 於 2018 年 3 月 6 日在康威生命遊戲論壇上公布，並於 3 月 8 日發佈到 Hacker News，獲得 733 分與 143 則留言；留言者引用論壇說法，稱其為 48 年來首個具有新斜率的基本飛船，並指出它出現在幾乎-knightship 之後 14 年。Life Wiki 將其編目為 282P6H2V1，社群成員回報已建好 eater 與偵測器，而 knightship 槍或滑翔機合成被判定可能難上數個數量級。找到該圖樣的 ikpx 與 MetaSAT 程式碼已發佈於 GitLab。