2021の逆向きライフゲーム

#puzzle 14 #sat 2 #taocp 2 #パズル 13 #ライフゲーム 1 #年のパズル 8

ライフゲームで5ステップ後に 2021 になるパターンを探してみた．

KnuthのTAOCP V4F6 Satisifiability には逆向きライフが題材として取り上げられている．

Knuthのプログラムを使って，以下が最終状態になる5ステップ前の初期状態を探してみた．

.................
.................
..***.***.***.*..
....*.*.*...*.*..
..***.*.*.***.*..
..*...*.*.*...*..
..***.***.***.*..
.................
.................

実行結果1

実行したコマンド列は以下の通りだ．

# サイズ9x18で5ステップの状態遷移(6状態)のCNFを作成
sat-life-grid 9 18 6 >/tmp/a.sat
# 最終状態(f)が上記のパターンになるCNFを作成
./taocpsat life pattern f <life-2021.txt >/tmp/b.sat
# 初期状態(a)の生存セルの個数が65以下とするCNFを作成
./taocpsat life threshold_bb 9 18 a:65 >/tmp/c.sat
# 3つのCNFを連結してKnuthのSATソルバーで解を求める
cat /tmp/a.sat /tmp/b.sat /tmp/c.sat | sat13 h11 >/tmp/x.out
# 解の表示
sat-life-filter </tmp/x.out

出力結果は以下のようになった．

(20153 variables, 82524 clauses, 208961 literals successfully read)
!SAT!
Altogether 1501372+431184888736 mems, 32446597 bytes, 19058145 nodes, 12662514 clauses learned (ave 57.6->32.8), 7452506 memcells.
(4160032 learned clauses were trivial.)
(15690 learned clauses were discarded.)
(39803 clauses were subsumed on-the-fly.)
(11 restarts.)

....................
.**.**.*.*..*.......
....***..*.*.*.****.
..***.*****..***....
..*.*...........**..
..*.*...*...*..*.*..
...**..**..***...*..
.......***..***.*...
..**...*......*.*...
.**.*....*...*...**.
....................

実行時間は約431ギガmem (約1537秒)
初期状態のrleファイル (Golly で開くことができる)

状態遷移は以下の通り．

→

実行結果2

初期状態(a)の生存セルが63以下，状態(b)で51以下，状態(c)で51以下，状態(d)で38以下，状態(e)で29以下の状態遷移も求めてみた．

(c)を初期状態とした場合，生存セルの個数の最小値は49である．しかし，49あるいは50以下を指定すると2つ前の状態が存在しない(指定したサイズの場合)．そのため51と指定している．

sat-life-grid 9 18 6 >/tmp/a.sat
./taocpsat life pattern f <life-2021.txt >/tmp/b.sat
./taocpsat life threshold_bb 9 18 e:29 d:38 c:51 b:51 a:63 >/tmp/c.sat
cat /tmp/a.sat /tmp/b.sat /tmp/c.sat | sat13 h12 | sat-life-filter

出力結果は以下のようになった．

(23895 variables, 106402 clauses, 276059 literals successfully read)
!SAT!
Altogether 1861389+34814428607 mems, 10576907 bytes, 1611572 nodes, 1121519 clauses learned (ave 51.0->21.3), 1866558 memcells.
(585311 learned clauses were trivial.)
(1616 learned clauses were discarded.)
(3644 clauses were subsumed on-the-fly.)
(84 restarts.)
....................
....*..**.*.*..**.*.
...*...***.**...**..
.....*...*.*.*..*...
..***..*.*.*.....*..
........*.*.*.*...*.
..**.*.....*.****.*.
....*..*...*.**.**..
.*...**..**.*...*...
...**.*..*.*...*..*.
....................