SAT-Suche fand Sir Robin, Conways Lifes erstes elementares Knightship seit 48 Jahren

48 Jahre lang bewegte sich jedes in Conways Game of Life bekannte elementare Raumschiff entweder orthogonal oder diagonal. Schräge Schiffe existierten zwar, aber nur als riesige, konstruierte Gebilde aus Gleitern und Schaltkreisen, wie der Waterbear, nicht als kompakte elementare Muster. Einige Spieler, die die Suche versucht hatten, bezweifelten, dass ein elementares schräges Schiff überhaupt existierte.

Brute Force war aussichtslos, und ebenso die naheliegende klügere Idee: genetische Suche. Nahezu jede zufällige Konfiguration in Life stirbt aus, die Evolution ist extrem empfindlich gegenüber Anfangsbedingungen, und die überwältigende Mehrheit des Suchraums hat Fitness null, sodass kein Gradient bleibt, den ein genetischer Algorithmus erklimmen könnte.

Der Entdecker machte stattdessen ein Erfüllbarkeitsproblem daraus. Ein Programm namens ikpx, Teil seines MetaSAT-Projekts, formulierte das Finden eines schrägen Gleiters als eine Menge von SAT-Bedingungen: die Life-Übergangsregeln, die Anforderung, dass sich das Muster alle sechs Generationen um zwei Zellen horizontal und eine Zelle vertikal verschiebt, die bewiesene Mindestperiode für diese Steigung und die Grenze des Suchbereichs. Heuristische Bedingungen, etwa die Suche nach einem langen und dünnen Schiff statt einer beliebigen Form, verkleinerten den Raum, und ikpx übergab den resultierenden Bedingungsklumpen an einen modernen SAT-Solver.

Der Solver gab Sir Robin zurück, im Life Wiki katalogisiert als 282P6H2V1: der erste elementare schräge Gleiter und das erste elementare Raumschiff mit einer neuen Steigung seit 48 Jahren, das sich mit der für seine Steigung maximal möglichen Geschwindigkeit bewegt. Der Code wurde veröffentlicht, Community-Mitglieder meldeten einen bereits gebauten Eater und Detektor, und die Entdeckung erzielte 733 Punkte und 143 Kommentare auf Hacker News.

Das Muster nicht per Brute Force durchsuchen oder evolvieren, sondern „es existiert ein Schiff mit dieser Verschiebung“ als SAT-Bedingungen kodieren und einen Solver suchen lassen

Die Kodierung von „finde ein Muster“ als Erfüllbarkeit übergibt die Suche an SAT-Solver, die durch jahrzehntelange Forschung überraschend leistungsfähig geworden sind.

Heuristische Bedingungen wie lang und dünn statt beliebiger Form entfernen die überwältigende Mehrheit des Kandidatenraums, ohne die Zielklasse auszuschließen.

Die Ausrichtung auf eine (2,1)-Verschiebung mit ihrer bewiesenen Mindestperiode von sechs Generationen bedeutete, dass die Suche auf das schnellstmögliche schräge Schiff zielte, sodass der erste Erfolg die 48-jährige Frage endgültig klärte.

Brute Force und genetische Suche hatten keinen Ansatzpunkt, weil fast jedes Life-Muster stirbt und kleine Änderungen kaskadieren, während die Constraint-Suche keinen Fitness-Gradienten benötigt.

Das Ergebnis war elementar und kompakt genug, um ein nützlicher Baustein zu sein, und der offene Code und interaktive Betrachter ermöglichten der Community, es zu verifizieren und darauf aufzubauen.

Wenn ein Suchraum keinen Gradienten und fast keine Überlebenden hat, sollte man ihn nicht blind abtasten: Existenz als Bedingungen kodieren, den Raum mit Domänen-Heuristiken verkleinern und einen Solver das Erkunden übernehmen lassen

Sir Robin wurde am 6. März 2018 in den Conway's-Life-Foren angekündigt und am 8. März auf Hacker News gepostet, wo es 733 Punkte und 143 Kommentare erzielte; Kommentatoren zitierten das Forum, das es als erstes elementares Raumschiff mit einer neuen Steigung seit 48 Jahren bezeichnete, und merkten an, dass es 14 Jahre nach dem Fast-Knightship kam. Das Life Wiki katalogisierte es als 282P6H2V1, Community-Mitglieder meldeten einen bereits gebauten Eater und Detektor, und eine Knightship-Kanone oder Gleiter-Synthese wurde als wahrscheinlich um Größenordnungen schwieriger eingeschätzt. Der ikpx- und MetaSAT-Code, der das Muster fand, wurde auf GitLab veröffentlicht.