Busca por SAT encontrou Sir Robin, a primeira knightship elementar do Jogo da Vida de Conway em 48 anos

Durante 48 anos, toda nave espacial elementar conhecida no Jogo da Vida de Conway se movia ortogonalmente ou diagonalmente. Naves oblíquas existiam, mas apenas como vastas estruturas projetadas montadas a partir de planadores e circuitos, como o Waterbear, não como padrões elementares compactos. Alguns jogadores que haviam tentado buscar duvidavam que uma nave oblíqua elementar existisse.

A força bruta era inútil, e também a ideia óbvia mais inteligente: busca genética. Quase toda configuração aleatória no Jogo da Vida morre, a evolução é extremamente sensível às condições iniciais, e a esmagadora maioria do espaço de busca tem aptidão zero, não deixando gradiente para um algoritmo genético escalar.

O descobridor, em vez disso, transformou o problema em um problema de satisfatibilidade. Um programa chamado ikpx, parte de seu projeto MetaSAT, formulou a busca por um planador oblíquo como um conjunto de restrições SAT: as regras de transição do Jogo da Vida, a exigência de que o padrão se desloque duas células horizontalmente e uma verticalmente a cada seis gerações, o período mínimo comprovado para essa inclinação, e a fronteira da região de busca. Restrições heurísticas, como buscar uma nave longa e fina em vez de uma forma arbitrária, reduziram o espaço, e o ikpx entregou a resultante pilha de restrições a um solucionador SAT moderno.

O solucionador retornou Sir Robin, catalogada no Life Wiki como 282P6H2V1: o primeiro planador oblíquo elementar e a primeira nave espacial elementar com uma nova inclinação em 48 anos, movendo-se na velocidade máxima possível para sua inclinação. O código foi publicado, membros da comunidade relataram um eater e um detector já construídos, e a descoberta atraiu 733 pontos e 143 comentários no Hacker News.

Não use força bruta nem evolua o padrão; codifique 'existe uma nave com este deslocamento' como restrições SAT e deixe um solucionador buscar

Codificar 'encontrar um padrão' como satisfatibilidade entrega a busca a solucionadores SAT que décadas de pesquisa tornaram surpreendentemente poderosos.

Restrições heurísticas como longa e fina em vez de forma arbitrária removem a esmagadora maioria do espaço de candidatos sem excluir a classe alvo.

Mirar um deslocamento (2,1) com seu mínimo comprovado de seis gerações significou que a busca visava a nave oblíqua mais rápida possível, de modo que o primeiro sucesso resolveu a questão de 48 anos de imediato.

Força bruta e busca genética não tinham tração porque quase todo padrão do Jogo da Vida morre e pequenas mudanças se propagam em cascata, enquanto a busca por restrições não precisa de gradiente de aptidão.

O resultado era elementar e compacto o suficiente para ser um bloco de construção útil, e o código aberto e os visualizadores interativos permitiram que a comunidade o verificasse e construísse sobre ele.

Quando um espaço de busca não tem gradiente e quase nenhum sobrevivente, não o amostre às cegas: codifique a existência como restrições, reduza o espaço com heurísticas de domínio e deixe um solucionador fazer a exploração

Sir Robin foi anunciada nos fóruns do Jogo da Vida de Conway em 6 de março de 2018 e publicada no Hacker News em 8 de março, atraindo 733 pontos e 143 comentários; comentaristas citaram o fórum chamando-a de primeira nave espacial elementar com uma nova inclinação em 48 anos e observaram que ela veio 14 anos após a quase-knightship. O Life Wiki a catalogou como 282P6H2V1, membros da comunidade relataram um eater e um detector já construídos, e julgou-se provável que um canhão de knightship ou uma síntese de planadores fosse ordens de magnitude mais difícil. O código ikpx e MetaSAT que encontrou o padrão foi publicado no GitLab.