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.)

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

状態遷移は以下の通り.

実行結果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.)
....................
....*..**.*.*..**.*.
...*...***.**...**..
.....*...*.*.*..*...
..***..*.*.*.....*..
........*.*.*.*...*.
..**.*.....*.****.*.
....*..*...*.**.**..
.*...**..**.*...*...
...**.*..*.*...*..*.
....................
  • 実行時間は約35ギガmem (約107秒). 各状態での生存セルの個数を制限すると,速くなる可能性があることがわかった.
  • 初期状態のrleファイル (Golly で開くことができる)

状態遷移は以下の通り.

リンク


関連するページ