SAT 탐색으로 콘웨이의 생명 게임에서 48년 만에 첫 기본 나이트 우주선 '서 로빈' 발견

48년 동안 콘웨이의 생명 게임에서 알려진 모든 기본 우주선은 직교 또는 대각선 방향으로 움직였다. 비스듬한 우주선은 존재했지만, 워터베어처럼 글라이더와 회로로 조립된 거대한 인공 구조물일 뿐이었고, 소형 기본 패턴은 아니었다. 탐색을 시도했던 일부 플레이어들은 기본 비스듬한 우주선이 존재하는지 자체를 의심했다.

무차별 대입은 희망이 없었고, 당연히 더 똑똑해 보이는 아이디어인 유전 탐색도 마찬가지였다. 생명 게임에서 거의 모든 무작위 배치는 소멸하고, 진화는 초기 조건에 극도로 민감하며, 탐색 공간의 압도적 다수가 적합도가 0이어서 유전 알고리즘이 올라갈 경사가 존재하지 않았다.

발견자는 대신 이를 충족 가능성 문제로 만들었다. 그의 MetaSAT 프로젝트의 일부인 ikpx라는 프로그램은 비스듬한 글라이더 찾기를 일련의 SAT 제약 조건으로 제시했다: 생명 게임의 전이 규칙, 패턴이 6세대마다 수평으로 2칸, 수직으로 1칸 이동해야 한다는 요구, 해당 기울기에 대해 증명된 최소 주기, 그리고 탐색 영역의 경계가 그것이다. 임의의 모양 대신 길고 얇은 우주선을 찾는 것과 같은 휴리스틱 제약이 공간을 줄였고, ikpx는 그렇게 만들어진 제약 조건 덩어리를 현대적인 SAT 솔버에 넘겼다.

솔버는 서 로빈을 반환했으며, 생명 위키에는 282P6H2V1로 등재되었다. 이는 최초의 기본 비스듬한 글라이더이자 48년 만에 새로운 기울기를 가진 최초의 기본 우주선으로, 해당 기울기에서 가능한 최대 속도로 움직인다. 코드가 공개되었고, 커뮤니티 구성원들은 이미 이터와 검출기가 만들어졌다고 보고했으며, 이 발견은 해커 뉴스에서 733점과 143개의 댓글을 받았다.

패턴을 무차별 대입하거나 진화시키지 말고, '이 변위를 가진 우주선이 존재한다'를 SAT 제약 조건으로 인코딩하여 솔버가 탐색하게 하라

'패턴을 찾아라'를 충족 가능성으로 인코딩하면 탐색이 수십 년의 연구로 놀라울 만큼 강력해진 SAT 솔버에게 넘어간다.

임의의 모양 대신 길고 얇은 것과 같은 휴리스틱 제약은 목표 클래스를 배제하지 않으면서 후보 공간의 압도적 다수를 제거한다.

증명된 6세대 최소 주기를 가진 (2,1) 변위를 목표로 삼았다는 것은 탐색이 가능한 가장 빠른 비스듬한 우주선을 겨냥했다는 뜻이며, 따라서 첫 성공이 48년의 질문을 단번에 해결했다.

무차별 대입과 유전 탐색은 거의 모든 생명 게임 패턴이 소멸하고 작은 변화가 연쇄적으로 증폭되기 때문에 실마리를 잡지 못했지만, 제약 조건 탐색은 적합도 경사가 필요 없다.

결과는 유용한 구성 요소가 될 만큼 기본적이고 소형이었으며, 공개된 코드와 대화형 뷰어 덕분에 커뮤니티가 검증하고 그 위에 쌓아 올릴 수 있었다.

탐색 공간에 경사가 없고 생존자가 거의 없을 때는 맹목적으로 표본을 뽑지 말고, 존재를 제약 조건으로 인코딩하고, 도메인 휴리스틱으로 공간을 줄이며, 솔버가 탐색하게 하라

서 로빈은 2018년 3월 6일 콘웨이의 생명 게임 포럼에서 발표되었고, 3월 8일 해커 뉴스에 게시되어 733점과 143개의 댓글을 받았다. 댓글 작성자들은 포럼을 인용하며 이를 48년 만에 새로운 기울기를 가진 최초의 기본 우주선이라고 했고, 거의-나이트 우주선 이후 14년 만에 나왔다고 언급했다. 생명 위키는 이를 282P6H2V1로 등재했고, 커뮤니티 구성원들은 이미 이터와 검출기가 만들어졌다고 보고했으며, 나이트 우주선 건이나 글라이더 합성은 수백 배 더 어려울 것으로 판단되었다. 패턴을 찾은 ikpx와 MetaSAT 코드는 GitLab에 공개되었다.