조합 최적화로 에덴의 정원 배치 증명

Advent Calendar 3일째 기사 조합 최적화로 폭격기 퍼즐 풀기
Advent Calendar 5일 기사 조합 최적화로 스테인드 글라스 풀기

이게 뭐야

에덴의 정원 배치를하고 있습니까?

에덴의 정원 배치는 셀 오토 마톤에서 다른 어떠한 배치로부터도 도달 할 수없는 배치를 지칭한다.
~~~~ 에덴의 정원 배치 - wikipedia

셀 오토마톤의 일종인 라이프게임 의 아래에 있는 에덴의 원 배치가 정말로 그런지 확인해 봅시다.

참고: Achim's Game of Life Page

조합 최적화에 사용되는 솔버는 모든 조합을 조사해 줍니다. 솔버에서 대답이 나오지 않는다는 것을 알면 에덴의 정원 배치임을 증명할 수 있습니다.

사고방식

라이프 게임에서 허용되는 조건을 수식으로 표현합니다.

현재 = 원시 :

과거 = 원시, 과거 주위 8 매스 = 2

과거 주위 8칸 = 3

현재 = 죽음 :

과거 주위 8칸<=1

과거 = 죽음, 과거 주위 8 매스 = 2

과거 주위 8칸>=4

OR 조건은 선형식으로 표현할 수 없으므로 0-1 변수를 사용하여 구분합니다.

참고: 퍼즐에서 볼 수있는 조합 최적화 기술 - IF 조건

파이썬 프로그램

이전 상태를 계산하는 프로그램(solve )은 다음과 같습니다.

파이썬

import pandas as pd, matplotlib.pyplot as plt
from pulp import LpProblem, LpStatus, lpSum, value
from ortoolpy import addbinvar, addbinvars
def solve(data):
    ni,nj = len(data),len(data[0])
    a = pd.DataFrame([(i,j,data[i][j]!='.') for i in range(ni)
        for j in range(nj)], columns=list('行列値'))
    a['Var'] = addbinvars(len(a))
    m = LpProblem()
    for _,r in a.iterrows():
        v = lpSum(a.query(f'{r.行-1}<=行<={r.行+1}&{r.列-1}<=列<={r.列+1}').Var)-r.Var
        if r.値: # 3 <= v+x, 2v+x <= 7
            m += v + r.Var >= 3
            m += 2*v + r.Var <= 7
        else: # v+x <= 2 or >=4
            y = addbinvar()
            m += v + r.Var <= 2 + 7*y # y==0 → v+x <= 2
            m += v         >= 4*y     # y==1 →   v >= 4
    m.solve()
    print(LpStatus[m.status])
    if m.status==1:
        a['Val'] = a.Var.apply(value)
        plt.imshow((a.Val<0.5).values.reshape(ni,nj), cmap='gray', interpolation='none')
        plt.show()

확인 그 1

먼저 solve가 이전 상태를 계산했는지 간단한 예를 확인해 봅시다.
(아래는 에덴의 원 배치가 아니라 글라이더입니다)

파이썬

solve("""\
.#.
#..
###""".splitlines())
>>>
Optimal

Optimal 그래서 솔루션이 존재합니다. 확실히, 그림의 상태로부터 1스텝 진행하면, 입력의 상태가 되는 것을 확인할 수 있습니다. solve가 이전 상태(중 하나)를 계산할 수 있음을 확인했습니다.

확인 2

파이썬

solve("""\
.##..#.##...
#..##..#.#.#
.#.#.##.#.#.
#....##..##.
.###...#....
..#.#.##.#..
.#.##...#.#.
#....#.#....""".splitlines())
>>>
Infeasible

이번에는 Infeasible 1입니다. 확실히 에덴의 정원 배치처럼 보입니다.

이상



2018/10/25, 필자의 PR에서 버그가 수정되어 「Infeasible」라고 표시되게 되었습니다. fix: issue-171, add MIP Infeasible status  ↩