La recherche SAT a trouvé Sir Robin, le premier vaisseau élémentaire de type cavalier en 48 ans dans le Jeu de la vie de Conway

Pendant 48 ans, tous les vaisseaux élémentaires connus dans le Jeu de la vie de Conway se déplaçaient soit orthogonalement, soit diagonalement. Des vaisseaux obliques existaient, mais seulement sous forme de vastes structures construites à partir de planeurs et de circuits, comme le Waterbear, et non sous forme de motifs élémentaires compacts. Certains joueurs qui avaient tenté des recherches doutaient même qu'un vaisseau oblique élémentaire existe.

La force brute était sans espoir, tout comme l'idée plus intelligente évidente : la recherche génétique. Presque toute configuration aléatoire dans Life meurt, l'évolution est extrêmement sensible aux conditions initiales, et l'écrasante majorité de l'espace de recherche a une fitness nulle, ne laissant aucun gradient à gravir pour un algorithme génétique.

Le découvreur en a plutôt fait un problème de satisfiabilité. Un programme appelé ikpx, faisant partie de son projet MetaSAT, a posé la recherche d'un planeur oblique comme un ensemble de contraintes SAT : les règles de transition de Life, l'exigence que le motif se déplace de deux cellules horizontalement et d'une verticalement toutes les six générations, la période minimale prouvée pour cette pente, et la frontière de la région de recherche. Des contraintes heuristiques, comme chercher un vaisseau long et fin plutôt qu'une forme arbitraire, ont réduit l'espace, et ikpx a remis la boule de contraintes résultante à un solveur SAT moderne.

Le solveur a renvoyé Sir Robin, catalogué sur le Life Wiki sous le nom 282P6H2V1 : le premier planeur oblique élémentaire et le premier vaisseau élémentaire doté d'une nouvelle pente en 48 ans, se déplaçant à la vitesse maximale possible pour sa pente. Le code a été publié, des membres de la communauté ont signalé qu'un eater et un détecteur étaient déjà construits, et la découverte a recueilli 733 points et 143 commentaires sur Hacker News.

Ne pas recourir à la force brute ni à l'évolution du motif ; encoder « il existe un vaisseau avec ce déplacement » sous forme de contraintes SAT et laisser un solveur chercher

Encoder « trouver un motif » comme un problème de satisfiabilité confie la recherche à des solveurs SAT que des décennies de recherche ont rendus étonnamment puissants.

Des contraintes heuristiques comme long et fin plutôt que forme arbitraire éliminent l'écrasante majorité de l'espace des candidats sans exclure la classe cible.

Cibler un déplacement (2,1) avec son minimum prouvé de six générations signifiait que la recherche visait le vaisseau oblique le plus rapide possible, de sorte que le premier succès a tranché définitivement la question vieille de 48 ans.

La force brute et la recherche génétique n'avaient aucune prise parce que presque tout motif de Life meurt et que de minuscules changements se propagent en cascade, tandis que la recherche par contraintes n'a pas besoin de gradient de fitness.

Le résultat était élémentaire et assez compact pour être un bloc de construction utile, et le code ouvert et les visionneuses interactives ont permis à la communauté de le vérifier et de s'appuyer dessus.

Lorsqu'un espace de recherche n'a pas de gradient et presque aucun survivant, ne l'échantillonnez pas à l'aveugle : encodez l'existence sous forme de contraintes, réduisez l'espace avec des heuristiques du domaine, et laissez un solveur faire l'exploration

Sir Robin a été annoncé sur les forums du Jeu de la vie de Conway le 6 mars 2018 et publié sur Hacker News le 8 mars, recueillant 733 points et 143 commentaires ; des commentateurs ont cité le forum le qualifiant de premier vaisseau élémentaire doté d'une nouvelle pente en 48 ans et ont noté qu'il arrivait 14 ans après le quasi-cavalier. Le Life Wiki l'a catalogué sous le nom 282P6H2V1, des membres de la communauté ont signalé qu'un eater et un détecteur étaient déjà construits, et un canon à vaisseau de type cavalier ou une synthèse par planeurs a été jugé probablement plus difficile de plusieurs ordres de grandeur. Le code ikpx et MetaSAT qui a trouvé le motif a été publié sur GitLab.