Una búsqueda SAT halló a Sir Robin, la primera nave de caballería elemental del Juego de la Vida de Conway en 48 años

Durante 48 años, toda nave espacial elemental conocida en el Juego de la Vida de Conway se desplazaba de forma ortogonal o diagonal. Las naves oblicuas existían, pero solo como vastas estructuras de ingeniería ensambladas a partir de planeadores y circuitería, como el Waterbear, no como patrones elementales compactos. Algunos jugadores que habían intentado buscarlas dudaban que existiera una nave oblicua elemental.

La fuerza bruta era inútil, y también lo era la idea obvia más inteligente: la búsqueda genética. Casi toda configuración aleatoria en Life muere, la evolución es extremadamente sensible a las condiciones iniciales, y la inmensa mayoría del espacio de búsqueda tiene aptitud cero, sin dejar gradiente alguno que un algoritmo genético pueda escalar.

El descubridor, en cambio, lo convirtió en un problema de satisfacibilidad. Un programa llamado ikpx, parte de su proyecto MetaSAT, planteó la búsqueda de un planeador oblicuo como un conjunto de restricciones SAT: las reglas de transición de Life, el requisito de que el patrón se desplace dos celdas horizontalmente y una verticalmente cada seis generaciones, el período mínimo demostrado para esa pendiente, y el límite de la región de búsqueda. Restricciones heurísticas, como buscar una nave larga y delgada en lugar de una forma arbitraria, redujeron el espacio, e ikpx entregó la maraña de restricciones resultante a un solucionador SAT moderno.

El solucionador devolvió a Sir Robin, catalogada en la Life Wiki como 282P6H2V1: el primer planeador oblicuo elemental y la primera nave espacial elemental con una nueva pendiente en 48 años, desplazándose a la máxima velocidad posible para su pendiente. El código se publicó, miembros de la comunidad informaron que ya se habían construido un comedor y un detector, y el descubrimiento atrajo 733 puntos y 143 comentarios en Hacker News.

No aplicar fuerza bruta ni evolución al patrón; codificar «existe una nave con este desplazamiento» como restricciones SAT y dejar que un solucionador busque

Codificar «encontrar un patrón» como satisfacibilidad entrega la búsqueda a solucionadores SAT que décadas de investigación han vuelto sorprendentemente potentes.

Restricciones heurísticas como larga y delgada en lugar de forma arbitraria eliminan la inmensa mayoría del espacio de candidatos sin excluir la clase objetivo.

Apuntar a un desplazamiento (2,1) con su mínimo demostrado de seis generaciones hizo que la búsqueda apuntara a la nave oblicua más rápida posible, de modo que el primer éxito zanjó la cuestión de 48 años de forma definitiva.

La fuerza bruta y la búsqueda genética no tenían tracción porque casi todo patrón de Life muere y los cambios diminutos se propagan en cascada, mientras que la búsqueda por restricciones no necesita gradiente de aptitud.

El resultado era elemental y lo bastante compacto como para ser un bloque de construcción útil, y el código abierto y los visores interactivos permitieron a la comunidad verificarlo y construir sobre él.

Cuando un espacio de búsqueda no tiene gradiente y casi no tiene supervivientes, no muestrearlo a ciegas: codificar la existencia como restricciones, recortar el espacio con heurísticas del dominio y dejar que un solucionador haga la exploración

Sir Robin se anunció en los foros de Conway's Life el 6 de marzo de 2018 y se publicó en Hacker News el 8 de marzo, atrayendo 733 puntos y 143 comentarios; los comentaristas citaron el foro, que la llamaba la primera nave espacial elemental con una nueva pendiente en 48 años, y señalaron que llegó 14 años después de la casi-nave de caballería. La Life Wiki la catalogó como 282P6H2V1, miembros de la comunidad informaron que ya se habían construido un comedor y un detector, y se juzgó probable que un cañón de naves de caballería o una síntesis de planeadores fuera órdenes de magnitud más difícil. El código ikpx y MetaSAT que encontró el patrón se publicó en GitLab.