日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

SAT ソルバを用いたライフゲームにおける物体の合成
手法
西村 春輝

長谷部 浩二セルオートマトンは，セルという小さな単位が互いに結合し相互作用を起こす数理モデルの一種である．その中でもコンウェイのライフゲームは，物体と呼ばれる特殊な性質を持ったパターンが出現することで知られており，新種の物体の生成手法についての研究が盛んに行われている．本研究では，充足可能性問題に依拠した近年の物体生成の手法を応用し，複数の物体を合成することによりキメラと称する新種の物体を生成する手法を提案する．その基本となるアイデアは，2 つの物体の断片を並べ，それらの間に適切なパターンを補完することで接合するというものである．これにより，物体全体を生成する場合と比べ探索範囲を大幅に削ることや，キメラ同士のキメラを作ることで全く新しい物体を作ることが可能になる．本研究では SAT ソルバを用いた実装で接合用のパターンを自動生成し，固定物体，振動子，移動物体の 3 つのカテゴリーを対象に実際に合成を行い提案手法の有効性を示す．

元し，SAT ソルバに解かせる手法 [5] が提案されてい1 序論

る．しかし，これらの物体生成の手法にはいくつかの

セルオートマトンは，セルと呼ばれる小さな単位が課題が存在する．De Bruijn の表や SAT ソルバを用連結し相互作用を起こすことで多様かつ複雑な振る舞いる手法は，特定の矩形範囲内に入る物体を全て網羅

いを見せる数理モデルである．中でも Conway が考的に探索できるという利点がある一方，条件を満たす案したライフゲーム [1] は，物体と呼ばれる特殊な性パターンを総当たりで探すのと本質的には同じこと質を持つパターンが出現することで知られている．ラをしており，物体のサイズが大きくなればその分だけイフゲーム内の物体は生物に似たその振る舞いから多探索に時間がかかる．この際に既存の物体の一部分をくの研究者の注目を集めている．また，Buckingham

利用することができれば計算量を減らせる可能性がらの研究 [2] が示すように計算機をライフゲーム内

あるが，利用した部分にどのような加工を施せば目的に構築する際に物体を回路の部品として利用可能での物体が得られるかについては不明な点が多い．

あることから，今もなお新種の物体を発見するため

本研究では，ライフゲームにおいて既存の物体が持の試みが多くなされている．例えば，Harold によりつ形状の規則性を利用し比較的大きなサイズの物体

De Bruijn の表を用いた手法 [3] が提案され，一部はを生成することを目的とする．より具体的には，既存

物体生成ツールとして実装されている [4]．近年ではの物体の断片に別のパターンや他の物体の断片を補Knuth により物体の生成問題を充足可能性問題へ還完することで，新しい種類の物体を生成する（本論文∗ Object Synthesis Method

in Game of Life Using

SAT SolverThis is an unrefereed paper. Copyrights belong to
the Author(s).
Haruki Nishimura, 筑波大学情報学群情報科学類, Collegeof Information Science, University of Tsukuba.
Koji Hasebe, 筑波大学システム情報系, Faculty of Engineering, Information and Systems, University ofTsukuba.

ではこれをキメラと呼ぶ）．ある断片に対して適用できる補間パターンは限られているが，本研究では近年の SAT ソルバを用いた物体生成の手法を拡張し，補間パターンの導出に応用する．実装の際 SAT ソルバ
として Z3py [6] を用い，固定物体，振動子，移動物体の 3 種類のカテゴリーのうちいずれか 1 つに分類される物体を中心に合成を試みたところ，全てのカテゴリーで合成に成功した．振動子を例にとると，周期(i, j) と表す．また時刻 t = 0, 1, 2, ...(∈ T = N) とす

2 の振動子の断片と周期 3 の振動子の断片の間にパる．ある時刻 t におけるセル (i, j) の状態（0 または

ターンを補完することで周期 6 の振動子を得られた．

1）を関数 σ : P × T → {0, 1} で定義し，その値を本研究の利点は主に 3 つ存在する．1 つ目にキメラ

xti,j と表す．このとき，P を領域とするライフゲームの生成では物体の一部分がすでに完成しており，同じとは，以下の条件を満たす σ（ライフゲームの規則とサイズの物体を何もないところから生成する場合とt呼ぶ）と，任意の i, j, t について xt+1
i,j = σ(xi,j ) を満比較して探索範囲が小さくなるため，より早く物体をたす領域 PLife の 2 つ組のこととする．

∑i+1
∑j+1
t


m=i−1
n=j−1 xm,n = 3)
 1 (if
 1 (if xt = 1 andi,jσ(xti,j ) =
∑i+1
∑j+1
t


m=i−1
n=j−1 xm,n = 2)



 0
otherwise

発見することが可能となる．2 つ目にキメラどうしのキメラを作り続けることで，元の物体とは全く違う形状の物体を漸進的に作っていくことが理論上可能であり，全く新しい物体を生成する際にも利用可能な手段となり得る．3 つ目に，共通の部品を持つ物体を比較することで，物体の形状が持つ大局的な規則性を知る

2. 2 ライフゲームの規則と論理式ことができる．

セルの状態を，1 を真として 0 を偽とするような本論文の構成は以下の通りである．第 2 節ではラ

真偽値とみなすことにより，ライフゲームの規則 σ

イフゲームの概要を示す．第 3 節では SAT ソルバを

は 9 つのセルの状態を引数にとって 1 つのセルの状用いた物体の合成手法について説明する．第 4 節で態を返す命題関数 δ に書き換えることが可能である．

は SAT ソルバとして Z3py を用いた際の物体の合成

本論文では，δ(V (xti,j )) = σ(xti,j ) (where V (xti,j ) =例を示す．第 5 節では先行研究について述べる．第 6(xti−1,j−1 , xti−1,j , xti−,j+1 , xti,j−1 , xti,j , xti,j+1 , xti+1,j−1 ,節では結論と今後の課題を述べる．

xti+1,j , xti+1,j+1 )) と定義する．

2 ライフゲームの概要

2. 3 物体

2. 1 ライフゲームの規則

ライフゲーム内のセルの状態のうち 1 を黒に，0 をセルオートマトンは，格子空間上に敷き詰められた白に対応させて毎時描画していくと，黒いパターンが複数のセルが周囲のセルの状態に応じて状態を変化

拡大と縮小を繰り返す様子を観察できる．その一方させるオートマトンの一種である．その中でもライフで，何度遷移させても形状が変化しない固定物体や，ゲームは，0 または 1 の状態をとるセルが 2 次元の格

p 回の遷移で元の形状に戻る振動子，p 回の遷移を通子空間に敷き詰められ，以下の 3 つの規則に従ってして移動しながら元の形状に戻る移動物体など，特殊

時間とともに遷移していく．

な性質を持った物体と呼ばれるパターンが出現するこ• 誕生：自身の状態が 0，周囲 8 セルのうちちょうとがある．固定物体は，任意の時刻 t における形状とど 3 セルの状態が 1 のとき，次の時刻でセルは 1

位置が時刻 t + 1 におけるそれと一致することから以に状態遷移する．

下のように定義できる．

• 生存：自身の状態が 1 であり，周囲 8 セルのう定義 2. （固定物体） 矩形範囲 R(⊆ PLife ) において，

ち 3 セルか 2 セルの状態が 1 のとき，次の時刻t
任意の t ∈ T と任意のセル (i, j) ∈ R で xt+1
i,j = xi,jでセルは 1 に状態遷移する．

すなわち σ(xti,j ) = xti,j が成立するとき，R を固定物

• 死滅：上記の 2 つの規則のいずれにもあてはま体と呼ぶ．

らないセルは，次の時刻で 0 に状態遷移する．

また振動子は，任意の時刻 t におけるパターンの形

すなわち，ライフゲームは以下のように定義できる．

状と位置が時刻 t + p のそれと一致することから，以定義 1. （ライフゲーム）自然数の集合 N に対して

下のように定義できる．

P ⊆ N × N を領域といい，P の i 行 j 列のセルを

定義 3. （振動子）

矩形範囲 R(⊆ PLife ) において，

t
任意の t ∈ T と任意のセル (i, j) ∈ R で xt+pi,j = xi,jすなわち σp(xti,j ) = xti,j が成立するとき，R を周期

mmax , mmin , nmax ,nmin , midu , midv , a, b, p ∈ N，midu < midv とする．
また 3 つの矩形範囲 R0 , R1 , R2 ⊆ PLife が存在し，p の振動子と呼ぶ．
なお σ p は，σ を p 回適用することを意味する．一p

般に，σ を遷移規則に用いるセルオートマトンでは，1 つのセルの状態を決定する際にその周囲 p セ
pルを参照することが分かっている．すなわち，σ は
2(2p + 1) 個のセルの状態を入力とする関数であり，2

σ p : S (2p+1) → S （ただし，S = {0, 1}）となる写

R2 = {(i, j) | mmin ≤ i ≤ mmax , nmin ≤ j ≤ nmax }とし，矩形範囲 Rl ,Rr ,Rb を以下のように定める．

• Rl = {(i, j) | mmin ≤ i ≤ mmax , nmin ≤ j ≤midu } について，Rl ⊆ R0
• Rr = {(i, j) | mmin ≤ i ≤ mmax , midv ≤ j ≤nmax } について，Rr ⊆ R1
• Rb = {(i, j) | mmin ≤ i ≤ mmax , midu + 1 ≤像である．
移動物体は，任意の時刻 t におけるパターンの形状
が時刻 t + p で一致し，かつ縦に a セル，横に b セル
移動していることから，以下のように定義できる．
定義 4. （移動物体）

定義 5. （物体の合成）

矩形範囲 R(⊆ PLife ) にお

い て ，任 意 の t ∈ T と 任 意 の セ ル (i, j) ∈ R で

j ≤ midv −1} について，Rb ̸⊆ R0 かつ Rb ̸⊆ R1
このとき，• Rl を R0 の 左 半 分 の 断 片 と い い ，セ ル の 列
Cl = {(i, midu ) | mmin ≤ i ≤ mmax } を，Rlの切り口と呼ぶ．

xti−a,j−b が• Rr を R1 の 右 半 分 の 断 片 と い い ，セ ル の 列成立するとき，R を周期 p，(a, b) 方向への移動物体

Cr = {(i, midv ) | mmin ≤ i ≤ mmax } を，Rr

xt+p
i,j

=

xti−a,j−b すなわち σ p (xti,j )

=

と呼ぶ．

の切り口と呼ぶ．

以上の定義から分かるように，固定物体は周期 1• Rb を Rl と Rr の補完パターンといい，2 つのセの特別な振動子であり，なおかつ周期 1，(0, 0) 方向

ルの列 Cbl = {(i, midu + 1) | mmin ≤ i ≤ mmax }への特別な移動物体である．また，振動子は周期 p，と Cbr = {(i, midv − 1) | mmin ≤ i ≤ mmax } を(0, 0) 方向への特別な移動物体であるといえる．

Rb の切り口と呼ぶ．
また，矩形範囲 Rs = {(i, j) | mmin − p ≤ i ≤3 物体の合成

mmax + p, nmin − p ≤ j ≤ nmax + p} において，全て

3. 1 補完パターンの (i, j) ∈ R で論理式

本論文で述べる物体の合成とは，同じ周期 p を持σ p (xi,j ) ↔ x(i−a),(j−b)

つ 2 つの断片の間にバッファとなる適切なパターン

が真になるとき，R2 を断片 Rl と断片 Rr の合成とを埋め込んでつなげ，新しい物体を作ることを指す．

定義する．

(1)

異なる周期を持つ 2 つの断片の合成は，両方の周期

定義 5 において矩形範囲 R2 の内部およびその周囲について公倍数をとり同一の周期にそろえることでp セルで式 (1) が成立していなくてはならないことに可能になる．接合によって生まれた新しいパターンがなっているが，実際には Rb の内部およびその周囲 p

周期 p の物体として成立するためには，パターン内

セルで式 (1) が成立するように Rb のパターンを選ぶ

部の全てのセル及びその周囲 p セルの領域において，だけで物体の合成が成功する．なぜなら，本研究では

σ で遷移させた際に状態が変わらないことが求めら

断片 Rl と Rr が既存の物体を半分に割ったものであれる．なぜなら，σ p 下ではあるセルの状態がその周る状況を想定しており，Rl や Rr に含まれるセルの囲 p セルの状態に影響を与えるからである．

うち矩形範囲 Rb の周囲 p セルより外に位置するもの

p

すなわち物体の合成は以下のように定義される．こでは既に式 (1) が成立しているからである．つまり，

こでは 2 つの物体を左右に並べて合成する場合のみ

Rb とその周囲 p セルの矩形範囲をまとめて Rm とすを定義するが，一般性を失うことなく，縦に 2 つに並るなら，以下の論理式が真になるよう Rb 内のセルのべた場合についても定義をすることができる．

状態を選んだとき合成が成功する．
∧ p
σ (xi,j ) ↔ xi−a,j−b (where (i, j) ∈ Rm )ついてセルの制約を作り論理積でつなげることで，補(2)完パターンの制約を表現できる．1 つのセルについて

なお，ある論理式を真にする変数の割り当ての有無，

制約を作るにはその周囲 1 セルの状態が必要である

及びその割り当ての具体的な内容を導出する問題は充から，ピンク枠内の 10×6 セルが参照される．水色枠

足可能性問題 [7] [8] と呼ばれている．この問題には割り当てを総当たりしなくてはならないケースがあり，NP 完全問題であることが知られている．しかし複数内のセルの状態は変数，その外にあるセルの状態は定数となる．ピンク色の領域の左上の角を (1, 1) とする
とき，補完パターンの制約は以下のように表される．
9 ∧5∧の節が連言でつなげられた CNF と呼ばれる論理式においては，DPLL や矛盾からの節学習など，変数の割り当てを高速で網羅したり探索範囲を削ったりする
ためのアルゴリズムが発見されており，それらを実装(δ(V (xti,j )) ↔ xti,j )(4)

i=2 j=2

このとき、(i, j) = (2, 5) のときのセルの制約は以下の論理式で表される。

した SAT ソルバと呼ばれるツールが実用化されてい0 ↔ δ(0, 0, 0, 0, 0, 0, xt3,4 , 1, 1)

る．上の論理式を CNF に変換し SAT ソルバに解か

また，(i, j) = (6, 4) のときのセルの制約は，以下のせることで，補完パターンが導出できるのである．

論理式で表される．

(5)

xt6,4 ↔ δ(xt5,3 , xt5,4 , 1, xt6,3 , xt6,4 , 0, xt7,3 , xt7,4 , 1) (6)3. 2 固定物体用の補完パターン
固定物体の場合補完パターンはその周囲 1 セルの内容に影響を与えるため，定義 2 を用いて固定物体の補完パターンを定義すると以下のようになる．
定義 6. （固定物体の補完パターン）ex , ey ∈ Nとし，Re ⊆ PLife かつ Re = {(i, j) | ey − 1 ≤ i ≤ey + m, ex − 1 ≤ j ≤ ex + n, m > 0, n > 0} と

図1なる大きさ (m + 2)(n + 2) の矩形範囲 Re におい

固定物体の接合例て，σ(xti,j ) = xti,j が全ての (i, j) ∈ Re で成立するとき，Rc ⊂ Re かつ Rc = {(i, j) | ey ≤ i ≤ey + m − 1, ex ≤ j ≤ ex + n − 1} となる大きさ m × nの矩形範囲 Rc を固定物体の補完パターンと呼ぶ．

3. 3 振動子用の補完パターン
振動子の補完パターンは，定義 3 より σ p : S → S

論理式 δ が σ と等価であることを利用すると，定義の上ではセルの状態が変化しない．補完パターンが6 より補完パターン Rc は以下の論理式を真にする．

周囲 p セルの状態遷移に影響を与えることを考慮す

∧

ey +m

ex
+n
∧

ると，振動子の補完パターンは以下のように定義さ(δ(V (xti,j )) ↔ xti,j )

i=ey −1 j=ex −1(where V (xti,j ) = {xti+u,j+v | −1 ≤ u, v ≤ 1})

れる．

(3)

これにより固定物体を合成する問題は，充足可能性
問題に変換される．なお，(3) の論理式を固定物体における補完パターンの制約と呼び，その中の論理式

δ(V (xti,j )) ↔ xti,j を固定物体におけるセルの制約と呼ぶ．
例えば，図 1 の 6×2 セルの水色枠内で補完パター
ンを作る場合，オレンジ枠内で示された 8×4 セルに

定義 7. （振動子の補完パターン）ex , ey , p ∈ N とし，Re ⊆ PLife かつ Re = {(i, j) | ey − p ≤ i ≤ ey +m+p−1, ex −p ≤ j ≤ ex +n+p−1, m > 0, n > 0}となる大きさ (m + 2p)(n + 2p) の矩形範囲 Re において，σ p (xti,j ) = xti,j が全ての (i, j) ∈ Re で成立するとき，Rc ⊂ Re かつ Rc = {(i, j) | ey ≤ i ≤ey + m − 1, ex ≤ j ≤ ex + n − 1} となる大きさ m × nの矩形範囲 Rc を振動子の補完パターンと呼ぶ．
論理式 δ p が σ p と等価であることを利用すると，

定義 7 より補完パターン Rc は以下の論理式を真に

3. 4 移動物体用の補完パターン

する．

移動物体の補完パターンは，定義 4 より σ p : S → S∧∧

i=ey −pj=ex −pey +m+p−1 ex +n+p−1を適用すると縦に a セル，横に b セル移動する．補(δ p (V (xti,j )) ↔ xti,j )完パターンが周囲 p セルの状態遷移に影響を与える(where V (xti,j ) = {xti+u,j+v | −p ≤ u, v ≤ p})(7)

これにより振動子を合成する問題は，充足可能性問
題に変換される．なお，(7) の論理式を周期 p の振動子における補完パターンの制約と呼び，その中の論理式 δ p (V (xti,j )) ↔ xti,j を周期 p の振動子におけるセルの制約と呼ぶ．

ように定義される．
定義 8. （移動物体の補完パターン）ex , ey , p, a, b ∈N とし，Re ⊆ PLife かつ Re = {(i, j) | ey − p ≤ i ≤ey + m + p − 1, ex − p ≤ j ≤ ex + n + p − 1, m >0, n > 0} となる大きさ (m + 2p)(n + 2p) の矩形範

例えば，図 2 の 7×3 セルの水色枠内で補完パター
ンを作る場合，オレンジ枠内で示された 11×7 セルについてセルの制約を作る必要がある．1 つのセルの制約を作る際に周囲 p セルの状態が δ p に代入されるた
め，ピンク枠内の 15×11 セルが参照される．水色枠
内のセルの状態は変数，その外にあるセルの状態は定数となる．ピンク色の領域の左上の角を (1, 1) とする
とき，補完パターンの制約は以下のように表される．

∧13 ∧9i=3ことを考慮すると，移動物体の補完パターンは以下の2ttj=3 (δ (V (xi,j )) ↔ xi,j )つ Rc = {(i, j) | ey ≤ i ≤ ey + m − 1, ex ≤ j ≤ex + n − 1, m > 0, n > 0} となる大きさ m × n の矩形範囲 Rc を周期 p，(a, b) 方向への移動物体の補完パターンと呼ぶ．
論理式 δ p が σ と等価であることを利用すると，定義 8 を用いて補完パターン Rc は以下の論理式を真に∧∧

i=ey −pj=ex −pey +m+p−1 ex +n+p−1

このとき，(i, j) = (9, 4) のときのセルの制約は以下の論理式で表される．

(δ p (V (xti,j )) ↔ xti−a,j−b )(where V (xti,j ) = {xti+u,j+v | −p ≤ u, v ≤ p}) (10)
これにより移動物体を合成する問題は，充足可能0 ↔ δ(1, 0, 0, xt7,5 , xt7,6 , 0, 0, 0, xt8,5 , xt8,6 , ...,
(8)

また，(i, j) = (6, 7) のときのセルの制約は，以下の論理式で表される．

性問題に変換される．なお，(10) の論理式を周期 p，(a, b) 方向への移動物体における補完パターンの制約と呼び，その中の論理式 δ p (V (xti,j )) ↔ xti−a,j−b を
周期 p の移動物体におけるセルの制約と呼ぶ．

xt6,7 ↔ δ(0, 0, 0, 0, 0, xt5,5 , xt5,6 , xt5,7 , 0, 0, ...,
xt8,5 , xt8,6 , xt8,7 , 0, 0)

が全ての (i, j) ∈ Re で成立するとき，Rc ⊂ Re かする．

(where V (xti,j ) = {xti+u,j+v | −2 ≤ u, v ≤ 2})0, 0, 1, xt11,5 , xt11,6 )囲 Re において，σ p (xti,j ) = xti−a,j−b (−p ≤ a, b ≤ p)

(9)
3. 5 補完パターンと物体の成立
周期 p，(a, b) 方向への移動物体から取り出された

2 つの断片を補完パターンで接合することにより，新しいパターンが生成される．これを本論文ではキメラと呼ぶ．キメラが周期 p，(a, b) 方向への移動物体であることは以下の定理を用いて示すことができる．
定理 1. （合成による物体の成立）矩形範囲 R(⊆ PLife )を 3 つ の 矩 形 範 囲 R0 , R 1 , R 2 を 含 む 矩 形 範 囲 とし，全ての (i, j) ∈ R0 ∪ R1 について σ p (xti,j ) =xti−a,j−b (−p ≤ a, b ≤ p) が成り立つとき，全ての
図2

周期 2 の振動子の接合例(i, j) ∈ R2 においても σ p (xti,j ) = xti−a,j−b が成り立つならば，矩形範囲 R は周期 p ,(a, b) 方向への移動

物体となる．

Proof. R0 , R1 , R2 の定義より R0 ∪ R1 ∪ R2 = R である．したがって，xti,j ∈ (R0 ∪ R1 ∪ R2 ) となる全ての (i, j) で σ p (xti,j ) = xti−a,j−b (−p ≤ a, b ≤ p)が成立しているとき，全ての (i, j) ∈ R について

σ p (xti,j ) = xti−a,j−b が成立する．定義 4 より，R は
周期 p ,(a, b) 方向への移動物体である．

2 つの物体の断片と補完パターンは，それぞれ先の定理における R0 , R1 , R2 に相当する．補完パターンは
定義 8 より，R0 と R2 の境界のパターンと R1 と R2のそれを変更しない．そのため全ての (i, j) ∈ R0 ∪ R1
について σ p (xti,j ) = xti−a,j−b (−p ≤ a, b ≤ p) が成立する．また定義 8 より，補完パターン内のセル(i, j) は全て σ p (xti,j ) = xti−a,j−b (−p ≤ a, b ≤ p)を満たす．したがって全ての (i, j) ∈ R2 において

図3

振動子の接合例

σ p (xti,j ) = xti−a,j−b (−p ≤ a, b ≤ p) が成立している．
よって定理 1 より，キメラは周期 p,(a, b) 方向への移

広い領域を定義 5 における断片とみなし部分的な合動物体である．

成を行った．次に (b) の断片の右端を周期 3 の振動

2 つの振動子の断片と補完パターンから成る複合体

子の一部とみなし，(c) のピンク枠内の部分と接合しも，定理 1 より振動子であることが証明される．なた．この際も，青枠で囲まれたより広い領域を定義 5

ぜなら，定理 1 において (a, b) = (0, 0) を代入する

における断片とみなし部分的な合成を行った．周期のことで証明できるからである．同様に，この定理に違う振動子を固定物体を介して合成することに成功

p = 1, (a, b) = (0, 0) を代入することで固定物体の断し，(d) に示す周期 6 の振動子を得た．1 回目の接合片と補完パターンから成るキメラが固定物体であるにおよそ 1 分，2 回目の接合におよそ 4 分 50 秒を要ことを証明できる．

した．

4 合成結果と考察
4. 1 実行環境

4. 3 移動物体の合成
以下では移動物体の合成例を示す．図 4 の (a),(b)

本研究では，命題関数 δ p とセルの制約の生成には，どちらも周期 2，(0,-1) 方向への移動物体である．

python ライブラリ Z3py を用い，また同ライブラリ

これらからピンク枠内の一部分を取出し青枠内で示を用いて補完パターンの制約を充足可能にする変数

した断片を作り，(c) に示すように水色枠内の補完パの割り当てを導出した．

ターンを間に挟んで周期 2，(0,-1) 方向への移動物体を得た．補完パターンの導出にはおよそ 1 分 50 秒か

4. 2 振動子の合成

かった．

以 下 で は 振 動 子 の 合 成 例 を 示 す．図 3 の 物 体(a),(b),(c) は ，そ れ ぞ れ 周 期 2 の 振 動 子 ，固 定 物

4. 4 考察

体，周期 3 の振動子である．初めに (b) の断片の左端

補完パターンの制約に基づき適切な接合が行える

を周期 2 の振動子の一部とみなして (a) のピンク枠

ことを確認した．特に振動子の合成において，固定物内の部分と接合した．その際に，青枠で囲まれたより

体を振動子として利用することで異なる周期を持つ

が可能になる．初めに D に属するパターンを横に 1
セルずつずらしながら重ねていき，横に細長いパターンを可能な限り多く作っておく．この際に De Bruijnの表が利用される．この表では D に含まれる 3×3 のパターンが大きさ 3×2 の小さなセグメント 2 つの接続規則に変換される．この接続規則にしたがってセグ
メントをつなげていくことで，3 × n の細長いパターンが生成される．次にこの 3×n のパターンを縦に 1
セルずつずらしながら重ねていき，固定物体を完成させる．この際にも De Bruijn の表が利用される．この表では 3×n のパターンが 2×n の小さなセグメン
トの接続規則に変換される．この接続規則に従ってセグメントを m − 1 回つなげていくことで，大きさm × n の固定物体が完成する．
図4

移動物体の接合例

De Bruijn の表を用いて物体を生成するツールとして D. Eppstein による gﬁnd [4] が知られており，移振動子の合成に成功しており，これを拡張すれば限り動物体の探索の際に De Bruijn の表が応用されていなく大きな周期の振動子を作ることができる．具体的

る．移動物体も振動子も，ある 2 次元セルオートマには，別々の周期を持つ振動子を大量に用意して，一トン下では固定物体としてふるまうため，De Bruijn

部分を切り取り固定物体を用いて列車のように連結の表を用いた物体の自動生成は他の種類の物体の生することにより，それらの周期が掛け合わさった周期成に応用可能である．

の長い振動子を得られる．合成結果の図を見ると補完パターンのサイズが断片と比較して同じくらいかそ

5. 2 SAT ソルバを用いた生成

れより大きくなっており，接合するためには断片同士

有界モデル検査 [9] とは，ある状態遷移系の遷移のの間隔が十分大きい必要があるとわかる．補完パター

パスが特定の性質を満たすかどうかを判定する手法のンの最小のサイズについてより詳しく調査する必要

1 つである．現実のシステムは際限なく状態遷移のパがあるといえる．また，各セルの制約を CNF（連言スが分岐して増えるため，それらのパスを 1 つずつ標準形）に変換するまでに時間がかかっているようで調べ性質を検査することは困難である．そこで有界モあり，Tseitin 変換や先行研究を参考にセルの制約をデル検査では，初期状態からの遷移を有限回数に抑え

効率よく CNF に変換する手段を探す必要がある．

有限な長さを持つパスについて性質を検査する．この検査においてパスが満たすべき性質は論理式で表現

5 関連研究され，この式の充足可能性を判定することで，当該の5. 1 De Bruijn の表を用いた物体生成

性質を持ったパスが存在するかどうかを確認できる．

De Bruijn の表 [3] は，ライフゲームの物体のうちKnuth は有界モデル検査で利用される論理式を応固定物体と呼ばれるものを生成するために使われる

用し，ライフゲームにおける物体の生成問題を充足表である．ライフゲームの固定物体に含まれる 3×3

可能性問題に変換する手法を提案した [5]．T (X, X ′ )セルの部分的なパターンは全て，ある 284 種類のパを，ライフゲームにおいて平面中のパターン X が X ′ターンの集合 D の要素になっていることが確定している．したがって，D からある要素を取出してそれに遷移するときに真を返す論理式であるとする．この∧(5. 2) は，パター
とき，論理式 n
k=1 T (Xk−1 , Xk )らを重ね合わせることで固定物体を組み立てること

ン X0 に n 回ライフゲームの規則を適用すると Xn になる際に真を返す．もし (5. 2) において (X0 = Xn )性が発見されるなら，それは 1 つの初期値に対してであるなら，この式は X0 が周期 n の振動子である

複数の分岐が存在するような規則であると思われる．

ときに真を返す論理式となり，この式を CNF に変換

なぜなら，ある同一の初期値を持つ 2 つの系に対しして SAT ソルバで解けば振動子の具体的なパターンてそのような規則を適用した場合，序盤の挙動は共通が求まる．ほかにも 5. 2 に対して様々な条件を追加

であるが途中から差異が生じ，最終的には別々の値にしたり変数の内容を変更したりすることで固定物体なるからである．例えばこの規則性は確率的 1 次元や移動物体，エデンの園などの導出に利用可能な論

セルオートマトンのような形態をとっていて，乱数で理式を得ることができる．なお，T (X, X ′ ) を CNF決めた初期値を代入して遷移させるとプロットした結に変換する手法が Knuth により提案されており [5]，果から移動物体を得られる可能性がある．このような

5. 2 を CNF に変換して SAT ソルバで利用すること

規則性が発見された場合，ただ単に物体の自動生成手

が容易になっている．また，5. 2 の論理式と SAT ソル

法として利用可能なだけでなく，ライフゲームの性質

バを用いて物体を探索するツールが実装されており，を解明するための手段となることが期待される．

例えば Cunningham による Logic Life Search [10] やGoucher による ikpx [11] などが知られている．
参 考 文 献6 まとめと今後の課題
本論文では，ライフゲームにおける物体の合成手法を提案した．その基本的なアイデアは，既存の物体の断片を並べ，隙間に適切なパターンを追加することで接合するというものである．断片の間に補完されるパターンが満たさなくてはならない制約は，パターンを構成する各セルの状態を変数にとる論理式として記述可能で，制約を満たすパターンが入力された際にこの論理式は真を返し，その逆で制約を満たしていないパターンに対して偽を返す．これにより，物体の合成
問題は充足可能性問題に還元され，SAT ソルバを用
いて解くことが可能になる．また本研究では SAT ソ
ルバとして Z3py を用いて簡易的な実装を行い，振動子の合成と移動物体の合成に成功した．
今後の研究としては，合成により大量に自動生成された物体から形状の規則性を抽出することを試みたいと考えている．同じ周期と移動方向を持つ物体
を 2 つ用意したとき，同一の構造が部分的に共有されつつそれ以外の部分では異なった構造をとっていることがある．そのため，もし物体の形状について規則[ 1 ] Schiﬀ, J. L. Cellular Automata A Discrete Viewof the World. John Wiley & Sons, Inc., 2008.
[ 2 ] Rendell, P. Turing machine universality of thegame of life. Springer, 2016.
[ 3 ] McIntosh, Harold V. Life’s still lifes. In Game ofLife Cellular Automata, pp. 35–50. Springer, 2010.
[ 4 ] Eppstein, D. gﬁnd 4.9 – search for gliders
in semitotalistic cellular automata. URL: https://www.ics.uci.edu/~eppstein/ca/gfind.c.
[ 5 ] Knuth, D.E. The Art of Computer Programming, Volume 4, Fascicle 6: Satisﬁability. AddisonWesley Professional, 2015.
[ 6 ] z3py-tutorial.
URL: https://github.com/
ericpony/z3py-tutorial.
[ 7 ] Moskewicz, M.W., Madigan, C.F., Zhao, Y.,
Zhang, L., and Malik, S. Chaﬀ: Engineering aneﬃcient sat solver. In Proceedings of the 38th annual Design Automation Conference, pp. 530–535,
2001.
[ 8 ] 井上克巳, 田村直之ほか. Sat ソルバーの基礎（＜特集＞最近の sat 技術の発展）. 人工知能学会誌,
Vol. 25, No. 1, pp. 57–67, 2010.
[ 9 ] 土屋達弘. 充足可能性判定を利用したモデル検査. コ
ンピュータ ソフトウェア, Vol. 29, No. 1, pp. 19–29,
2012.
[10] Cunningham, O. logic-life-search. URL: https://github.com/OscarCunningham/logic-life-search.
[11] Goucher, A.P. metasat. URL: https://gitlab.
com/apgoucher/metasat.