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

グラフ書換え系におけるグラフ構造の効率的な一意バイト列生成手法
宮原 和大

上田 和紀

グラフ書換え系をモデリング言語とするモデル検査は高い表現力と対称性吸収機能を備えているが，その処理の過程で構築したグラフ構造の管理においてグラフ同型性判定を頻繁に行う．グラフ構造の一意バイト列生成はグラフ同型性判定の手法の一つであり，多数のグラフ間の同型性を判定する際に有効である．したがって，グラフ書換え系におけるグラフ構造の一意バイト列の効率的な生成は重要な課題といえる．本研究では彩色単純グラフにおける一意バイト列生成手法に用いられる McKay のグラフ正規化アルゴリズムにおいて，グラフ書換え処理に伴うグラフ構造の差分情報を活用することによる最適化手法を考案した．本論文では考案した McKay のグラフ正規化アルゴリズムのグラフ書換え系向きの最適化手法と時間計算量の改善について述べる．

異の有無を見ることによりグラフ構造の同型性を判

1 はじめに定するものである．n 個のグラフ構造間の同型性判定

グラフ書換え系はモデリング言語に用いられる系

においては，同型性の判定のためのグラフ構造の探索の一つであり，与えられた書換え規則にしたがってグ処理がもっとも時間計算量を必要とするものであり，

ラフ構造の一部を書き換えることにより処理の進行

通常のグラフ同型性判定は各グラフの２つ組に対しを表現するものである．グラフ書換え系を用いたモデて探索を実行するため O(n2 ) 回のグラフ構造の探索

リング言語には階層グラフ書換え言語 LMNtal [3] やを行う必要があるが，一意バイト列生成によるグラフ

Bigraph [6]，GROOVE [8] などがあり，一般に代数的同型性判定はバイト列生成のための O(n) 回の探索のもしくは組み合わせ論的構造を多項式時間でグラフ構みで可能であり多数のグラフ間の同型性を判定する

造にエンコードできる [7] [2] [5] ことから，これらのモ際に有効である．

デリング言語は高い表現力と対称性吸収機能を備えてしたがって，グラフ書換え系におけるグラフ構造

いるといえる．しかし，このようなモデリング言語での一意バイト列の効率的な生成は重要な課題である．

記述されたモデルに対してモデル検査を行う際にはそグラフ書換え系に限らない彩色単純グラフ（2. 1 節参の処理の過程で構築したグラフ構造の管理のために頻照）における一意バイト列生成手法としては，McKay

繁なグラフ同型性判定を必要とし，その同型性判定ののグラフ正規化アルゴリズム [4] [1] により得られる正処理時間がモデル検査の処理時間を大きく左右する．

規形のバイト列への変換などが挙げられるが，これまグラフ構造の一意バイト列生成はグラフ同型性判

でグラフ書換え処理に最適化された一意バイト列の定の手法の一つである．この手法は各グラフ構造に一対一対応するバイト列を生成して，そのバイト列の差
Optimized Canonical Graph Labeling Algorithm for
Graph Rewriting Systems.
Kazuhiro Miyahara, 早稲田大学大学院基幹理工学研究
科情報理工学専攻, Waseda University.
Kazunori Ueda, 早稲田大学理工学術院情報理工学科,
Waseda University.

生成手法はまだ提案されていない．
本論文ではグラフ書換え処理に伴うグラフ構造の差分情報に着目し，McKay のグラフ正規化アルゴリ
ズムに対するグラフ書換え前のグラフ構造の正規形
生成時に得た情報と差分情報の活用によるグラフ書
換え後のグラフ構造の正規形生成の時間計算量の改善手法を述べる．

ここで本論文の構成を述べる．

る m(≤ n) に対して k ≤ m のとき φ−1 (k) ̸= ∅ か

第 2 節では本論文の研究内容に関連する定義を述

つ m < k ≤ n のとき φ−1 (k) = ∅ であるような関数

べる．特に 2. 5 節で述べる探索グラフ，2. 6 節で述べ

φ : V −→ Ω = {1, 2, ..., n} である．すなわち，頂点る拡張隣接，2. 7 節で述べる書換え距離は本論文独自に塗る m 色の色を 1 から m の自然数を割り当てるの概念となっている．第 3 節では McKay のグラフ正ことで表現する．

規化アルゴリズムの概要を述べ，続く第 4 節では第 2

また，彩色クラス (color-class) とは Wi [φ] = {v ∈節で定義した拡張隣接の概念と McKay の正規化アルV | φ(v) = i} のことであり，ここで特に |Wi [φ]| = 1

ゴリズムにおける処理との関係に関する定理を述べであるような彩色クラスを一元彩色クラスとよぶこる．第 5 節では McKay の正規化アルゴリズムにおいととする．すなわち，彩色クラスとは同じ彩色であるて書換え処理への最適化を行う箇所に関する性質をような頂点の集合である．

述べ，第 6 節で提案アルゴリズムの実現のために管また，C(V ) を V の彩色の全体とする．

理すべき情報と管理のためのデータ構造に関して述

ここで，Sym(V ) を V 上の置換の集合，すなわちべる．第 7 節では提案アルゴリズムの内容に関して

V 上の対称群として，φ ∈ C(V ), v ∈ V, g ∈ Sym(V )述べ，第 8 節で具体的な例題における本来の McKayについて，φg (v) = φ(v gの正規化アルゴリズムと提案アルゴリズムの時間計算量に関して考察する．

−1) とする．

さらに，彩色グラフとはグラフ X とその彩色 φ の組 (X, φ) である．なお，本論文においては彩色グラ
フは異なる次数の頂点に対しては異なる彩色を与え

2 定義

るものを扱うものとする．

以下，特に断りのない限りグラフ (graph) とは有限無向単純グラフ (finite and simple graph) の事を

2. 2 同型性

指すものとし，彩色グラフ (colored graph) とは 2. 1

K(V ) を V を頂点集合とするグラフ全体の集合と節で定める頂点彩色グラフ (vertex-colored graph) を指すものとする．単純グラフとは自己ループや多重辺を含まないグラフである．
本論文では有限無向単純グラフに対象を定めて議論する．
グ ラ フ X = (V, E) と g ∈ Sym(V ) に つ い て ，{u, v} ∈ E に対し {u, v}g = {ug , v g } として X g =(V, E g ) とする．

フなどに対しても彩色に反映する内容を対応させるこ

X, Y ∈ K(V ) が同型 (isomorphic) であるとは，∃g ∈ Sym(V )[Y = X g ] であることとし X ∼= Y と表とで同様のアルゴリズムを考えることが可能である．

記する．また，このときの g を X, Y 間の同型写像とLMNtal などのグラフ書換え系においてもそのグラフよぶ．

を行うが，有向グラフや辺にラベルを持つようなグラ構造の性質を彩色に反映することで適用可能である．

K(V ) × C(V ) を V 上の彩色グラフの全体とする．

また，グラフ X に対して V(X) は X の頂点集合(X, φ), (Y, ψ) ∈ K(V ) × C(V ) が同型であるとはを表し，E(X) は X の辺集合を表すものとする．
なお，2. 1 節，2. 2 節，2. 3 節，2. 4 節は文献 [7] を参考にした．対して 2. 5 節，2. 6 節，2. 7 節に関して∃g ∈ Sym(V )[Y = X g , ψ = φg ] であることとし(X, φ) ∼= (Y, ψ) と表記する．また，このときの g を(X, φ), (Y, ψ) 間の同型写像とよぶ．

は本研究のために新たに定めたものである．

2. 3 頂点分類 (naive vertex classification)
2. 1 頂点彩色 (vertex coloring)X = (V, E) をグラフとする．また，|V | = n とする．
このとき，頂点集合 V の彩色 (coloring) とは，あ頂 点 集 合 V と そ の 彩 色 φ : V −→ Ω に つ いて ，彩 色 φ′ が φ の 細 分 化 (refinement) で あ る とは ∀u, v ∈ V [φ(u) < φ(v) ⇒ φ′ (u) < φ′ (v)] であることとする．したがって，φ の細分化 φ′ は φ において別の彩色であった頂点同士は別の彩色のまま，同じ

さらに，v から距離 δ 以下の探索で到達する X の彩色であった頂点のいくつかに別の彩色を与えたもの

部分グラフ Sδ (v) を次で定め，半径 δ の探索グラフ

である．

と呼ぶこととする．なお，e ∩ Dδ−1 (v) ̸= ∅ とは e はまた，φ が V から Ω への全単射であるとき，φ はDδ−1 (v) に端点を持つことを意味する．

離散的 (discrete) であるという．すなわち，彩色 φ が離散的であるとはすべての頂点が一元彩色クラスにV(Sδ (v)) = Dδ (v)属することに等しい．

|V | = n な る グ ラ フ X = (V, E) と そ の 彩 色
φ : V −→ Ω に対して，各 v ∈ V に対し di (v) を彩色 i を持つ v の隣接ノードの個数とし，D(v) =E(Sδ (v)) =(φ(v), d1 (v), d2 (v), ..., dn (v)) とする．D(v) を辞書式に比較し順序付けの番号を彩色とすることで φ(v) の



∅






(δ = 0){e ∈ E | e ∩ Dδ−1 (v) ̸= ∅}





(δ > 0)

細分化 φ′ (v) を得ることができる．φ(0) = φ として，

φ(i+1) を φ(i) に上記の方法で得られる細分化とすれば，φ(r) = φ(r+1) となる r が r < n において必ず存在する．このような最初の φ(r)を φ と表記し，φ の安定細分化 (stable refinemnt) とよぶ．また，φ = φであるとき，φ は安定であるという．

2. 6 拡張隣接 (extended connectivity)
探索グラフの記憶なしでの深さ n の深さ優先探索で得られる情報を表現する概念を定める．

(X, φ) を彩色グラフとする．また，|V | = n とする．
頂点 v の距離 δ の有限拡張隣接とは以下で定める

2. 4 頂点の等価性

ECδ (v) とする．ただしここで {|...|} は多重集合を表X = (V, E) をグラフとする．

現するものとする．

v, w ∈ V について，v と w が X 上で等価であると


φ(v)






は，X 上の自己同型写像 g により v g = w となることする．
また，彩色グラフ (X, φ) において，v と w が (X, φ)ECδ (v) =上で等価であるとは，(X, φ) 上のの自己同型写像 g
により v g = w となることする．

2. 5 探索グラフ
McKay のグラフ正規化アルゴリズムは隣接する頂点への情報の伝播を繰り返すことにより構造の解析(δ = 0)(φ(v), {|ECδ−1 (w) | w ∈ adj(v)|})





(δ > 0)

また，EC∞ (v) = ECn (v) と定め，これを頂点 vの拡張隣接とする．
一般に互いに等価な頂点は等しい拡張隣接をもつが，を行う．そこで伝播回数に対する解析の及ぶ範囲を表

図 1 のグラフの頂点 A と頂点 C のように等しい拡張

現する概念を定める．

隣接をもつ頂点同士が互いに等価であるとは限らない．

X = (V, E) をグラフとする．v, w ∈ V について，

ただし，図 1 の彩色は全頂点で 1 とする．このとき各頂

v と w をつなぐ最短路に含まれる辺の個数を X 上の点の EC0 と EC1 および EC2 は 1 と (1, {|1, 1, 1|}) お

v と w の間の距離 (distance) とよび，∂(v, w) と表記

よび (1, {|(1, {|1, 1, 1|}), (1, {|1, 1, 1|}), (1, {|1, 1, 1|})|})

する．ただし，v と w が同じ連結成分に属していなである．

い場合には ∂(v, w) = ∞ とする．

対して，図 2 の構造のように等しい拡張隣接をもまた，Dδ (v) = {w ∈ V | ∂(v, w) ≤ δ} とする．すつような頂点の組が存在しないグラフ構造も存在す

なわち，Dδ は距離 δ 以内の頂点を表すものである．

る．ただし，図 2 の彩色は各頂点の次数とする．図 2

表1

図 2 における各頂点の有限拡張隣接

頂点

EC0

EC1

EC2

F

1

(1, {|3|})(1, {|(3, {|1, 2, 3|})|})

C

2(2, {|3, 3|})(2, {|(3, {|1, 2, 3|}), (3, {|2, 2, 3|})|})

A

2(2, {|3, 3|})(2, {|(3, {|2, 2, 3|}), (3, {|2, 3, 3|})|})

D

3(3, {|1, 2, 3|})(3, {|(1, {|3|}), (2, {|3, 3|}), (3, {|2, 3, 3|})|})

B

3(3, {|2, 2, 3|})(3, {|(2, {|3, 3|}), (2, {|3, 3|}), (3, {|2, 3, 3|})|})

E

3(3, {|2, 3, 3|})(3, {|(2, {|3, 3|}), (3, {|1, 2, 3|}), (3, {|2, 2, 3|})|})

ついて Sδ (v) = S1 (v) ∪ F∪Sδ−1 (w) であるw∈adj(v)G

ので，ECi (v) は Si (v) から一意的に定まることがわ

D

かる．

2. 7 書換え距離C

E

探索グラフの範囲内の構造がグラフ書換え処理による変化が起きたか否かを判断するために，頂点 v が書換え処理を受けた箇所からどれほどの距離にあるかを表す概念を定める．

B

A

グラフ書換えにおける書換え前の彩色グラフ(X1 , φ1 ) と書換え後の彩色グラフ (X2 , φ2 ) に関し

Hて，頂点 v ∈ V(X2 ) の書換え距離とは以下で定まる
図1

拡張隣接が等しいが等価でない頂点を含むグラフ

ϱ(v) である．
(i) v ∈ V(X2 ) \ V(X1 ) のとき ϱ(v) = 0

F(ii) v ∈ V(X2 ) ∩ V(X1 ) かつ φ1 (v) ̸= φ2 (v) のと

E

D

A

き ϱ(v) = 0(iii) v ∈ V(X2 ) ∩ V(X1 ) かつ φ1 (v) = φ2 (v) かつC

B

書換え前後のグラフの辺集合の対称差 E(X1 ) △E(X2 ) に v を 端 点 に 持 つ 辺 が 存 在 す る と き
図2

拡張隣接が全て異なるグラフ

ϱ(v) = 1(iv) (i),(ii),(iii) により ϱ が定まる頂点の集合を V ′の有限拡張隣接の一部は表 1 のようになる．

として，v ∈ V(X2 ) \ V ′ について

また，グラフ X の部分グラフの集合){Yi | i ∈ I}(∪∪∪
V(Yi )
について部分グラフ
Yi を V
Yi =
i∈I
i∈I
i∈I
)
(
∪
∪
Yi =
E(Yi ) により定めると，δ > 0 にとE

ϱ(v) = min{ϱ(w) + ∂(v, w) | w ∈ V ′ }

i∈I

i∈I

グラフ Y, Z について部分グラフ Y ∩ Z を V(Y ∩Z) = V(Y )∩V(Z) と E(Y ∩Z) = E(Y )∩E(Z) により定めるとすると，δ < ϱ(v) について Sδ (v) ⊆ X1 ∩ X2
であり Sδ (v) は書換えを受けないことがわかる．

2, φ(F ) = 2, φ(C) = 3, φ(G) = 3, φ(B) =(A|D|F|G|C|B|H|E)

4, φ(H) = 4, φ(E) = 5 を表すものである．
探索木の根は π の安定細分化であり，また節点の(A|D,F|C,G|B,H|E)(A|F|D|C|G|H|B|E)

彩色 φ について φ が離散的であればこれを探索木の葉とし，φ を終端彩色 (terminal coloring) とよぶ．

(B|G|D|E|F|A|H|C)(C|F|H|A|E|B|D|G)

例 え ば 図 3 に お け る (A|D|F |G|C|B|H|E) や(B|G|D|E|F |A|H|C) などは終端彩色である．

(C|F,H|A,E|B,D|G)(C|H|F|E|A|D|B|G)

φ が離散的でなければ，大きさ 2 以上の彩色クラ
スのうち彩色の値が最小な Wi から１つのグラフ頂点(D|G|B|A|H|E|F|C)

v を選択し新たな彩色を与えることで一元彩色クラス(A,B,C,D,E,F,G,H)(E|B|H|G|C|D|F|A)

として分離しその安定細分化を得る．これを v のスタ(E|B,H|C,G|D,F|A)

ビライザー (stabilizer) と呼び φv と表記する．φ の(E|H|B|C|G|F|D|A)(F|C|H|A|B|E|D|G)

子節点は各 v ∈ Wi のスタビライザー φv であり |Wi |個ある．

(G|B|D|E|A|F|H|C)(G|B,D|A,E|F,H|C)

例えば図 3 における (A|D, F |C, G|B, H|E) を φ とすると，W2 からグラフ頂点を選択することとなる．

(G|D|B|A|E|H|F|C)(H|C|F|E|D|A|B|G)

選択 D に対して (A|D|F |C, G|B, H|E) の安定細分化(A|D|F |G|C|B|H|E) が D のスタビライザー φD であり，選択 F に対して (A|F |D|C, G|B, H|E) の安定

図3

図 1 のグラフに対する McKay のグラフ正規化ア
ルゴリズムの探索木

細分化 (A|F |D|C|G|H|B|E) が F のスタビライザー

φF である．|W2 | = 2 より (A|D, F |C, G|B, H|E) の子は φD と φF の２つである．

なお，書換え距離の計算は幅優先探索により容易に可能である．

隣接行列の辞書式順序による比較により max{ψ :終端彩色 } を考えることで一意的な離散的彩色を得ることができる．

3 McKay のグラフ正規化アルゴリズム

McKay のグラフ正規化アルゴリズムにおいてはさ

McKay のグラフ正規化アルゴリズムは与えられたらに終端彩色同士の比較で得られる自己同型写像を

彩色グラフ (X, π) に対して辞書式順序において最大用いて探索木の枝刈りを行うことで一意的な離散的となる隣接行列を持つような π の一意的な離散的彩彩色の計算の効率化を行うこととなるが本論文では

色と自己同型群の探索を行うものである．π の一意的省略する．

な離散的彩色が得られれば，そこからの正規形や一意バイト列の生成は容易い．

McKay のグラフ正規化アルゴリズムは安定な彩色を節点とする探索木の深さ優先探索により行われる．
（図 3）
ただし，図 3 において各節点に記述されているのは対応する彩色の内容であり，“, ” は左右の頂点が4 拡張隣接と細分化
この節では本論文の研究内容に関連する定理を述べる．なお，各定理の証明は付録 A にて行う．
次の定理は安定細分化を得る過程での彩色の進行
が有限拡張隣接による情報を反映していることを示すものである．

同じ彩色であることを，“|” は右の頂点の彩色が左の頂点の彩色よりも真に大きいことを表す．すなわ
ち (A|D, F |C, G|B, H|E) とは φ(A) = 1, φ(D) =定理 4.1 (X, φ) を彩色グラフとする．このとき，∀k ∈ N, ∀v, w ∈ V(X)F

[ECk (v) = ECk (w)⇔ φ(k) (v) = φ(k) (w)]
E

となる．
I
D

続く定理は，一定以上の深さの有限拡張隣接が無限の深さの拡張隣接に対応する十分な情報を持っていることを表すものである．

C
B

A

定理 4.2 (X, φ) を 彩 色 グ ラ フ と す る ．ま た ，H|V(X)| = n とする．このとき，G∀v, w ∈ V(X)
[EC∞ (v) = EC∞ (w)

図4⇔ ∀m ≥ n[ECm (v) = ECm (w)]]

書換え処理適用前のグラフとなる．
上の定理から，次の系が示される．この系は安定細∀v1 , w1 ∈ V(X1 ), ∀v2 , w2 ∈ V(X2 )∼ (Si (v2 ), φ2 )[(Si (v1 ), φ1 ) =∧(Si (w1 ), φ1 ) ∼= (Si (w2 ), φ2 )分化で得られた彩色が拡張隣接による情報を反映していることを示すものである．

(i)

(i)

⇒ (φ1 (v1 ) ≤ φ1 (w1 )
(i)

(i)

⇔ φ2 (v2 ) ≤ φ2 (w2 ))]系 4.1 (X, φ) を彩色グラフとして，∀v, w ∈ V(X)
[EC∞ (v) = EC∞ (w) ⇔ φ(v) = φ(w)]となる．
上の定理より，有限拡張隣接 ECi が Si によってのみ定まるという次の系が示される．

となる．
系 4.2 彩色グラフ (X1 , φ1 ), (X2 , φ2 ) について，したがって，各頂点 v について安定細分化 φ は

Dn (v)，すなわち属する連結成分全体の影響を受けている．

∀v1 ∈ V(X1 ), ∀v2 ∈ V(X2 )[(Si (v1 ), φ1 ) ∼= (Si (v2 ), φ2 )⇒ ECi (v1 ) = ECi (v2 )]次の定理は，各頂点同士の彩色 φ(i) における大小となる．

関係が探索グラフ Si によってのみ決定されることを示すものである．

以上より，McKay のグラフ正規化アルゴリズムにおけるグラフ書換え処理の影響を考えると，初回の安定理 4.3 彩色グラフ (X1 , φ1 ), (X2 , φ2 ) について，

定細分化の過程での φ(i) は各頂点 v について Si (v)での構造のみで決定され，表 2 のように Si (v) 内に書換え箇所が含まれていなければ書換えの前後で細分化の大小関係は同じものとなる．対して，初回の安定表2

初期彩色を次数により行った図 4 と図 5 の初回安定細分化の比較（下線太字は φ(i) において Si (v) が変化したノード）

細分化

書換え前彩色

書換え後彩色φ(0)(A, F |G, H, I|B, C, D, E)(A, F |G, H, I, J|B, C, D, E)

φ(1)(A, F |I|G, H|C, D|B, E)(A|F |I|G, H|J|C, D|E|B)

φ(2)(A, F |I|G|H|C|D|B|E)(A|F |I|G|H|J|C|D|E|B)

φ(3)(F |A|I|G|H|C|D|B|E)

F

5 初回安定細分化処理とグラフ構造
系 4.1 より，McKay のグラフ正規化アルゴリズム

Jの初回安定細分化処理終了後の彩色クラスは各頂点の拡張隣接により定まる．
閉路グラフや完全グラフを含む正則グラフなどのE

拡張隣接が等しい頂点が多く存在する図 1 のような
DI構造においては初回安定細分化にいたるための細分化の回数は少なく，McKay のグラフ正規化アルゴリ

A

ズムの処理の大部分の時間を探索木の生成に費やすCBこととなる．
対して拡張隣接が等しい頂点が少ない図 2 のようHGな構造においては初回安定細分化はほぼ離散的であり，処理の大部分の時間を初回安定細分化の取得に費

図5

書換え処理適用後のグラフ

やすこととなる．
本論文において提案する手法は初回安定細分化の細分化終了以降の彩色はその頂点の属する連結成分

時間計算量の改善を図るものであるので，特に後者のの全体に依存しており，書換え処理が属する連結成分

ような構造において効果を発揮するものである．

に対して行われていればグラフ書換え処理の前後で反映される情報が異なっている．さらにはスタビライ

6 探索グラフ情報の保持ザーのための頂点の選択は直接グラフの幾何学的構

提案アルゴリズムではグラフ書換え前の構造にお造を反映したものではないので書換えの前後での彩

ける初回安定細分化で得られる各 Si (v) と彩色の細分

色の変化の予想が困難である．

化の進行の情報を保持しておき，グラフ書換え後の構

そこで，グラフ書換え前の構造に対する McKay のグラフ正規化アルゴリズム適用時に各頂点 v におい造に対する初回安定細分化の際に活用することで時間計算量の改善を図る．

て Si (v) の構造に関する情報を検出・保持し，グラフ

本節では，まず彩色の細分化の進行情報の保持の方書換え後の構造に対する McKay のグラフ正規化アル法について触れる．これによりグラフ書換え前の構造

ゴリズムの初回安定細分化適用時にこれらを利用すにおいて行われた彩色の細分化を計算せずに再現することで時間計算量の改善を図る．

ることを可能とし，グラフ書換え後の構造に対するア
ルゴリズムの適用時にはグラフ書換えの前後で割り当てられる彩色が変化する頂点についてのみ彩色の計算を行えば十分となる．

表3

図 4 の初回安定細分化の進行情報と図 5 の初回安定
細分化

続いて，彩色そのものの保持の方法に関して触れ（下線太字は Si (v) が変化したノード）

る．これは彩色が変化した頂点の彩色の計算を行う際に隣接する頂点の彩色を利用するためのものである

細分化

彩色

が，従来の McKay の正規化アルゴリズムにおける 1

初期値(J,∞ F,3 A,0 I,1 G,2 H,0 C,2 D,1 B,2 E)からの自然数を割り振る彩色ではグラフ書換えにより

φ(0)(F,3 A|0 J ,∞ I,1 G,2 H|0 C,2 D,1 B,2 E)

φ(1)(A|1 F |0 I|1 G,2 H|1 J |0 C,2 D|1 E|1 B)

φ(2)(A|1 F |0 I|1 G|2 H|1 J|0 C|2 D|1 E|1 B)

彩色の番号付けが影響を受けてしまう．そこで，ハッシュ関数を応用したグラフ書換えの影響を受けない彩色の基準を紹介する．
最後に彩色の細分化の進行情報とハッシュ値を保持

表4

図 5 の初回安定細分化の進行情報と図 4 の初回安定
細分化

し，表現するためのデータ構造としてのトライ木の仕（下線太字は Si (v) が変化したノード）様について触れる．これらを用いたアルゴリズムに関しては第 7 章で紹介する．

6. 1 彩色の細分化の進行情報(i)定理 4.3 より，φにおいて書換えの前後で彩色の大小関係が変化する頂点は Si (v) が変化した頂点 v のみであるが，彩色の細分化の計算には v に隣接する頂

細分化

彩色

初期値

(A,1 F,0 I,1 G,2 H,0 C,2 D,1 E,1 B)

φ(0)(A,1 F |0 I,1 G,2 H|0 C,2 D,1 E,1 B)

φ(1)(A,∞ F |0 I|1 G,2 H|0 C,2 D|1 E,∞ B)

φ(2)(A,∞ F |0 I|1 G|2 H|0 C|2 D|1 E|2 B)

φ(3)(A|3 F |0 I|1 G|2 H|0 C|2 D|1 E|2 B)

点の φ(i−1) における彩色も参照する．そのため，書換え後の構造の初回細分化 φ(i) の計算の時点までは(i−1)

書換え前の細分化 φを再現できる情報を保持す

ついても同様に書換え距離 1 以下の J, E, F 以外の頂点に関しては ”,1 ” であった箇所がそのまま ”|1 ” として彩色の区別になり，J, E, F はそれぞれ φ(0) におい

る必要がある．
ここで，φ(i) (v) < φ(i) (w) となった際には j ≥ i においても φ(j) (v) < φ(j) (w) となるので，書換え前のて同じ彩色となっていたものの中で図 5 の構造における φ(1) で定まる大小関係の位置に納まる．

構造での初回安定細分化時に 2 頂点間で別彩色となっ

以上より，書換え後の初回細分化の計算は φ(i) にた最小の段階数を何らかの形で保持しておくことにおいて，Si (v) が変化した頂点のみ φ(i−1) で同彩色より再現に十分な情報を保持することが可能である．

であったものの中での彩色の大小関係を計算すればよ

初期値 (J,∞ F,3 A,0 I,1 G,2 H,0 C,2 D,1 B,2 E)（表く，ほかの頂点は書換え前の細分化の進行をそのまま

3）は書換え前の構造における彩色の細分化の進行に採用すればよい．また，Si (v) が変化した頂点であっ関する情報を表現している．”,i ” は書換え前においても φ(i−1) において一元彩色クラスの元である場合て両端の頂点の彩色が φ(i) において区別されたことには彩色の再計算は必要ない．

を，”|i ” は書換え後において両端の頂点の彩色が φ(i)において区別されたことを表す．なお，∞ は安定細6. 2 ハッシュ値による彩色情報

分化時の彩色が等しいこと，もしくは細分化進行情報

表 3 における φ(2) において，頂点 D は S2 (D) ががないことを表す．

書換えにより変化しており，C においては S2 (C) は

また，表 4 は逆向きの書換え処理に関して表 3 と変化していない．ここで φ(2) の計算のために D(D)と D(C) の比較が必要となるが，書換え前の φ(2) に同様の表記を施したものである．
表 3 について，φ(0) を見ると書換え距離 0 の J 以外

関しては D(C) = (4, 0, 0, 1, 1, 1) であり，書換え後のの頂点に関しては ”,0 ” であった箇所がそのまま ”|0 ”

φ(2) では D(C) = (6, 0, 0, 0, 1, 0, 1, 0, 1) と変化してとして彩色の区別になっていることがわかる．φ(1)にいる．したがって，C に関しても彩色の値の比較のために D の計算をする必要が生じている．これは彩色表5が得られた順序に関して 1 から小さい順に番号付けをすることにより得られていることにより，全体の構

図 4 のハッシュ値による初回安定細分化

color (0)color (1)color (2)造に変化が生じると彩色の大小関係が維持されていE

050C5D1C

47AB1DC0

782F13C0ても番号付けが変化してしまうためである．

B

050C5D1C

47AB1DC0

79262E9D

color (3)C

050C5D1C

A017F61E

07F71192

したがって，グラフ書換え処理における再計算のD

050C5D1C

A017F61E

5B55B197

ためには v の φ(i) での順序の決定に用いられる値がG

050C5D1D

49FE7685

2F30B695

Si (v) から一意的に決定されるような値である必要がH

050C5D1D

49FE7685

67863F59I

050C5D1D

8F4C200Aあり，また Si (v) が異なる際には異なる値であること

A

050C5D1E

54F3BE57

C29FBDB0301177A3が望ましい．そこで，Si (v) をハッシュ値に変換してF

050C5D1E

54F3BE57

C29FBDB0

AC6ADF55

ハッシュ値を比較することで新たな彩色を得ることを考える．
以下のように関数 color (n) : V(X) −→ N を定め

表6

図 5 のハッシュ値による初回安定細分化（下線太字は変化したハッシュ値）

る．ただし，hash : {X ∈ NN | X is f inite} −→ N

color (0)color (1)はハッシュ値の有限多重集合に対するハッシュ関数とB

050C5D1C

47AB1DC0

する．

E

050C5D1C

95E9A3E3

color

(n)



φ(v)





(v) =

(n = 0)
hash{|color(n−1) (w) | w ∈ adj(v)|}





(n > 0)

ここで，δ > 0 について EC の定義より，color (n) (v)は ECn (v) から一意的に定まるため，Sn (v) から一意的に定まるものである．

ることにすると，φ′D (v) = (φ′ (i−1)=φ(0)(v), color′ (i)

計算された color

050C5D1C

A017F61E

07F71192

050C5D1C

A017F61E

98A107FE

J

050C5D1D

14284B30

G

050C5D1D

49FE7685

2F30B695

H

050C5D1D

49FE7685

67863F59I

050C5D1D

8F4C200AA

050C5D1E

54F3BE57

F

050C5D1E

D5941C89

する．
さらに，計算中の構造において Si (v) に対するハッと表記す

φ(w) ⇔ EC∞ (v) = EC∞ (w) ⇔ φ′ (v) = φ′ (w) でとし i > 0 についてはあるので，安定細分化の彩色クラスは等しいものと(i)(v)) の辞書式な比較に

より大小関係の決定を行えばよい．また，各頂点 v は
(i)

C
D

シュ値の値に衝突が起こらなかった場合，φ(v) =ハッシュ値による i 回目の細分化を φ′ (0)color (2)なる．
ハッシュ値 の 衝 突 に 関 し て は ，安 定 細 分 化 の 彩(v) を保持しておくことにする．

色 ク ラ ス が 決 定 さ れ る ス テップ 数 r に 対 し て ハ

表 5 と表 6 に見られるように，グラフ書換え後にッシュ値列 (color (0) (v), color (1) (v), ...color(r) (v)) とおいて Si (v) が変化していなければ書換え後の構造(color (0) (w), color(1) (w), ...color(r) (w)) が完全に一においても color(i)(v) の値は変化しないので，その致する際にのみ安定細分化の彩色クラスが従来のまま細分化に利用することが可能となる．なお，表 5

McKay の正規化アルゴリズムのものより大きなものと表 6 では color(0)はハッシュ値の分散のため適当な値に処理している．
また，その性質から安定細分化はとなる．したがって，単純なハッシュ値よりも衝突率は低いものとなる．拡張隣接が同じものも異なるもの
もハッシュ値列が一致したものは等しい安定彩色とし(color (0) (v), color(1) (v), ..., color(r) (v)) の辞書式なて扱い，McKay の正規化アルゴリズムの探索木生成

比較で得られる順序構造に等しく，これを φ′ と表記の根として用いることでハッシュ値の衝突を含むようなグラフ構造であっても一意な離散的細分化彩色を得
050C5D1Cることが可能である．
な お ，(color (0) (v), color (1) (v), ...color (r) (v)) と47AB1DC0

A017F61E

050C5D1D

49FE7685

050C5D1E

8F4C200A

54F3BE57(color (0) (w), color(1) (w), ...color(r) (w)) のうち
color(i) (v) ̸= color (i) (w) と な る よ う な 最 小 の iに 頂 点 v, w 間 の 彩 色 の 細 分 化 の 進 行 情 報 が 対
応 す る ．(color(0)(v), color(1)(v), ...color(r)

782F13C0

79262E9D

07F71192

5B55B197

2F30B695

67863F59

E

B

C

D

G

H

I

C29FBDB0301177A3

AC6ADF55

AF(v)) =(color (0) (w), color(1) (w), ...color(r) (w)) であるとき
は進行情報は ∞ である．

図6

図 4 の構造の安定細分化終了時の有限トライ木

6. 3 データ構造

状態として i = 0 から順に有限トライ木の i + 1 段目，

ハッシュ値列をキーとした辞書式順序による頂点のすなわち φ′(i)を書換え後の彩色グラフにおける正当保持のためにトライ木を用いて頂点を管理することな状態に変化させていくことで実行される．ただし，とする．

初期状態として用いる有限トライ木は書換えによりトライ木の根（0 段目）から延びるエッジは初期彩色である color(0)= φ をラベルとして管理し，以下 i

段目から延びるエッジは color(i)をラベルとする．す

消去された頂点を取り除き，新たに追加された頂点は有限トライ木の根ノードに持たせておくものとする．
（図 9）

なわち，トライ木の i + 1 段目は i 回目の細分化の状

基本的な処理の内容は書換え距離の計算による不態に対応しており，頂点 v, w 間の彩色の細分化の進正な状態である可能性のある頂点の判定，およびそれ

行情報は v と w の最長の共通なプレフィックスの長らの頂点の回収，正当な位置への再挿入からなる．

さに等しい．
（図 6）
ここで，ハッシュ値列は無限の長さを持つためトラしたがって，アルゴリズムの適用は i = 0 からはじ
め φ′

(i)

が離散的になるか細分化が進行しなくなるま

イ木は仮想的に深さ無限のものを扱うが細分化は有で以下の操作を繰り返すものである．
（図 10，図 11，

限回数以降は進行しないため有限の深さのトライ木

図 12）構造により表現が可能である．すなわち，一元彩色
クラスに対応するトライ木のノード以下の子ノード(i) ϱ(v) = i となる頂点 v を有限トライ木の深さ iは保持せず，また彩色が進行しなくなる深さ以下の子までさかのぼったノードに持たせる．この際，さノードも保持しない．以降は仮想的無限トライ木と有かのぼることにより不要となる有限トライ木の限トライ木を考えていく．

ノードは削除する．

なお，各トライ木のノードにおけるエッジの管理は(ii) 頂点をもつノードに関して，それが頂点を一

平衡 2 分木で行う．すなわち，実装上はこのトライ木つのみ持つ葉ノードでない場合には持つ頂点のは三分探索木により頂点の保持を行うものである．

それぞれに color (i) を計算し対応する子ノードに渡す．

7 差分情報適用アルゴリズム
提案する差分情報を活用した初回安定細分化取得(iii) 終了条件を判定し，終了しない場合には i を1 増加させ，(i) に戻る．

アルゴリズムを図 7，図 8 に示す．
例えば，図 4 から図 5 への書換え時における動7. 1 細分化の進行

作 を 考 え る ．i = 0 で は ϱ(v) = 0 な る 頂 点 が な差分情報を活用する初回安定細分化のアルゴリズム

いため (i) での頂点の回収は起こらず，(ii) においては書換え前の彩色グラフにおける有限トライ木を初期

color (0) (J) = 050C5D1D により J は真ん中の子ノーRequire: 書換え後の初回安定細分化有限トライ木 trie
Ensure: 書換え前彩色グラフ (X1 , φ1 ) 書換え後彩色グラフ (X2 , φ2 ) 書換え前の初回安定細分化有限トライ木 trie
for v ∈ V(X1 ) \ V(X2 ) dotrie.delete(v )end fortrie.root.vertexes := getNewVertexes()
halfwayVertexes := trie.root.vertexes
nextHalfwayVertexes := {}i := −1
repeati++reverseStack := getRewriteDistanceVertexes(i)while notEmpty(reverseStack ) dov := reverseStack .pop
tmpNode := v .owner
tmpNode.vertexes := tmpNode.vertexes \ {v}
if tmpNode.depth > i thenhalfwayVertexes.push(v )end ifwhile tmpNode.depth > i do
if isEmpty(tmpNode.vertexes) thentmpNode.delete()
end iftmpNode := tmpNode.parent
end while
tmpNode.vertexes.push(v )end while
while notEmpty(halfwayVertexes) dov := halfwayVertexes.pop
if notLeaf (v .owner )or notSingleton(v .owner .vertexes) thencolor := getColor (v , i)
if isExistChild(v .owner , color )and isLeaf (v .owner .child[color ]) thennextHalfwayVertexes:= nextHalfwayVertexes∪ v .owner .child[color ].vertexes
end ifv .owner .child[color ].vertexes.push(v )v .owner .vertexes = v .owner .vertexes \ {v}nextHalfwayVertexes.push(v )end ifend whilehalfwayVertexes:= nextHalfwayVertexes
until ¬isDiscrete(i − 1 ) and isRefined(i)if ¬isDiscrete(i − 1 ) and ¬isRefined(i) thencollectExtraNodes(trie, i)
end ifreturn trie
図7

差分適用初回安定細分化アルゴリズム

Require: 有限トライ木 trie
Ensure: 有限トライ木 trie ，整数 ifor v ∈ V(X2 ) do
tmpNode := v .owner
tmpNode.vertexes := tmpNode.vertexes \ {v}while tmpNode.depth > i + 1 do
if isEmpty(tmpNode.vertexes) thentmpNode.delete()
end iftmpNode := tmpNode.parent
end while
tmpNode.vertexes.push(v )end forreturn trie
図8

離散的な彩色が得られなかった際の終了処理

collectExtraNodes(trie, i)

J
050C5D1C

47AB1DC0

A017F61E

050C5D1D

49FE7685

8F4C200A

782F13C0

79262E9D

07F71192

5B55B197

2F30B695

67863F59

E

B

C

D

G

H

図9

050C5D1E

54F3BE57I

C29FBDB0301177A3

AC6ADF55

AF

図 4 から図 5 への書換え時の安定細分化における有限トライ木の初期状態

ドへ渡される．i = 1 では ϱ(E) = 1, ϱ(F ) = 1 より(i) で E と F は深さ 1 まで有限トライ木をさかのぼったノードへと渡される．このとき A もプレフィックスを共有する F がさかのぼったことにより不要なノードの分はさかのぼっている．
（図 10）回収を受けた

E, F と i = 0 で親ノードから渡された J については(ii) において color (1) (J) = 14284B30, color (1) (E) =95E9A3E3, color (1) (F ) = D5941C89 によりそれぞれ 対 応 す る 子 ノ ー ド へ と 渡 さ れ る ．i = 2 で はϱ(D) = 2 より (i) で D は深さ 2 まで有限トライ木をさかのぼったノードへと渡される．
（図 11）i = 1 で親ノードから渡された J, E, F についてはすでに一元彩
色クラスに属しているためこれ以上処理を行わず，回収された D は (ii) において color (1) (D) = 98A107FEにより対応する子ノードへと渡される．ここで，i = 2

7. 2 終了条件判定
050C5D1C

050C5D1D

E

このアルゴリズムの終了判定には isDiscrete(i − 1 )050C5D1E

J

47AB1DC0

A017F61E

49FE7685

および isRefined (i) が用いられている．これらの判

F
8F4C200A

54F3BE57

定方法と時間計算量について述べる．
まず，補助関数 otherDiscrete(i) について述べる．

79262E9D

07F71192

5B55B197

2F30B695

67863F59

B

C

D

G

H

I

A

otherDiscrete(i) は真偽値を返す関数であり φ′(i)の時点で halfwayVertexes に格納されていない頂点がすべて一元彩色クラスに属しているとき，かつそのと図 10

図 4 から図 5 への書換え時の i = 1 での (i) 計算

きに限り真となるものである．
この関数の計算のためにデータとして，各頂点が後における有限トライ木の状態

一元彩色クラスに属することとなった最初の φ′(i)のi の分布を表現する配列 Distribution と，その分布
050C5D1C

050C5D1D

050C5D1E

14284B30

49FE7685

8F4C200A

が 0 でない最大のインデックス max idx を保持する．

Distribution[i] は有限トライ木の深さ i+1 にある一元
47AB1DC0

95E9A3E3

A017F61E

54F3BE57

D5941C89

A

F

彩色クラスに対応した葉ノードの個数に一致する．たE

79262E9D

D

J

07F71192

B

C

2F30B695

67863F59G

H

I

だし，配列 Distribution は halfwayVertexes に格納されている頂点の個数はカウントしない．Distributionの更新は頂点の回収と挿入の処理の際に行えばよ

図 11

図 4 から図 5 への書換え時の i = 2 での (i) 計算

く，一回の処理はインクリメントおよびデクリメン
トにより実現されるため全体の計算量に影響しない．

後における有限トライ木の状態

max idx の更新も Distribution[max idx ] の値の更新の際や，i > max idx における REPEAT 文の処理

47AB1DC0

79262E9D

95E9A3E3

E

A017F61E

07F71192

98A107FE

CD

J

050C5D1C

050C5D1D

050C5D1E

14284B30

49FE7685

8F4C200A

2F30B695

67863F59GHの際に行えばよく，増加はインクリメントで行われ，

I

54F3BE57

D5941C89

A

F

また，減少は O(i) になりうるが一元彩色クラスに新たに追加された頂点は以降削除されないので減少は一度でも増加が起きてからは発生しない．したがってB減少処理は全体として REPEAT 文の実行回数を下
図 12

図 4 から図 5 への書換え時の安定細分化計算後における有限トライ木の状態回るため，これも全体の計算量に影響しない．
こ の よ う に 保 持 し て お い た max idx に つ い て ，otherDiscrete(i) は i ≥ max idx であるか否かを返せの深さですべての頂点が一元彩色クラスに属していばよいので計算量は O(1) である．なお，Distribution

る状態となったためアルゴリズムの適用は終了する．

と max idx は有限トライ木とともに次回の初回安定

このとき得られている有限トライ木は書換え後のグ

細分化処理時に持ち越す．また，空なグラフにおラフ構造の安定細分化に対応した仮想的無限トライ

いて Distribution はすべての値が 0 の配列であり，木を表現したものとなっている．
（図 12）

max idx = −1 であるものとする．さらに，初回安定

この処理で離散的な初回安定細分化が得られなかっ

細分化により一元彩色クラスに属さなかった頂点の表た場合には通常の McKay のグラフ正規化アルゴリズ

現のため Distribution は ∞ もインデックスとして許ムにおける探索木の生成を適用することで一意的な容し，Distribution[∞] は有限トライ木の一元彩色ク

離散的彩色を得る．

ラスに対応しない葉ノードに保持された頂点の個数に一致する．また max idx はそのような頂点が存在した時には ∞ であるとする．
′ (i)Increase[i] > 0 である限り i とともにインクリメンの時点で頂点がすべて一元彩トされるのみである．したがって，増加処理は全体と色クラスに属しているとき，かつそのときに限り真として REPEAT 文の実行回数を下回り全体の計算量なる関数である．

に影響しない．また，減少処理も高々有限トライ木のisDiscrete(i) は φ

halfwayVertexes に格納されていない頂点に関しては otherDiscrete(i) により判定が可能である．また halfwayVertexes に格納されている頂点は i + 1
における REPEAT 文の実行直後には φ′(i)

エッジの削除回数しか起こらないため全体の計算量に影響しない．
こ の よ う に 保 持 し て お い た Increase に つ い て ，で一元

isRefined (i) は Increse[i ] > 0 であるか否かを返せ

彩色クラスに含まれていないようなもののみであばよいので，計算量は O(1) である．なお，Increase

る．したがって i + 1 における REPEAT 文の実行と max depth は有限トライ木とともに次回の初回

直後において isDiscrete(i) = otherDiscrete(i) and

安定細分化処理時に持ち越す．また，空なグラフ

isEmpty(halfwayVertexes) により判定が可能である．

に お い て Increase は す べ て の 値 が 0 の 配 列 で あしたがって isDiscrete(i) に必要な時間計算量は O(1)り，max depth = −1 であるものとする．さらに，となる．

Increase は ∞ をインデックスとして許容せず，ま′ (i)isRefined (i) は，φよりも φ′ (i+1)が真に細かいた max depth は必ず有限であるとする．初回安定

彩色であるとき，かつそのときに限り真となる関数で細分化により彩色が離散的とならなかったときにはある．ただし，ここで φ同じ彩色 φ′ (−1)′ (−1)

はすべての頂点に対し(v) = 1 を割り当てるようなものであるとする．
この関数の計算のためにデータとして，各 φ′

max depth は処理終了時の i である．
max idx と max depth について，前者は初回安定細分化により離散的となる深さを，後者は実際に初(i−1)

回安定細分化を計算した深さを表す．したがって，初への増加量を表現する配列 Increase と回安定細分化により彩色が離散的となった場合にはIncrease が正の値を保持している最大インデックス

max idx = max depth となり，そうでない場合には

′ (i)

から φ

max depth を保持する．Increase[i] は仮想的無限ト

max idx = ∞ であり max depth は細分化が進行しライ木の深さ i + 1 にあるノードの個数から深さ i になくなった深さとなる．

あるノードの個数を除いたものに一致する，ただし一
元彩色クラスに対応するノードからは無限の深さまで子ノードが一つずつ伸びているものとする．すなわ
ち，彩色の増加数に等しい．これは仮想的に最初の有限個のみが正の数であるような無限配列 Increase を

表7

図 4 における終了条件判定情報（図 6 参照）

index

0

1

2

3

Distribution

0

1

6

2

max idx = 3

Increase

2

2

3

1

max depth = 3

表現するものであり，i > max depth について仮想的に Increse[i] = 0 である．Increase の更新は有限トライ木のノードのエッジの追加と削除の処理の際に行えばよく，一回の処理はインクリメントおよびデ

表8

図 5 における終了条件判定情報（図 12 参照）

クリメントにより実現されるため全体の計算量に影

index

0

1

2

響しない．max depth の更新も，エッジの削除によDistribution

0

5

5

max idx = 2

り生じた Increase[k ] = 0 となるような k に応じた減Increase2

52

max depth = 2

少と i の進行に応じた増加を施すこととなるが，後述するように Increase[i] = 0 となれば処理が終了する
ことにより減少は初めて i = max depth となるまでしか起こらず，また i = max depth となって以降は

E(1)

F(3)

D(1)

A

A(2)

B
C(1)

図 13

E

B(1)

C

書換え処理適用前のグラフ

E(1)

F

図 15

F(1)

D(1)

D

図 13 に対応する有限トライ木

A(1)
A,F

C(1)

B(1)
B

図 14

E

書換え処理適用後のグラフ

7. 3 終了後の正当性処理

CD

書換え後のグラフが初回安定細分化により彩色が離散的にならないとき，終了判定は isRefined (i) が

図 16

図 14 に対応する有限トライ木に正当性保持のため偽となることで起こるが，書換え前のグラフの初回安の処理を加える直前のもの

定細分化処理で得られた有限トライ木の深さが i + 1
よりも大きかった場合，i + 1 より深い位置に格納さ限トライ木の構造の性質上複数のエッジをもつノード

れている頂点についてはハッシュ値列の正当性が確に対する削除は頂点一つの削除について一回のみで認されていない状態である．
（図 15，図 16）したがっあるといえるので，頂点一つあたりのさかのぼり全体て，有限トライ木の持つ情報の正当性を維持するためでかかる時間計算量は O(n) である．したがって，正にそのような頂点を深さ i + 1 まで回収する必要があ

当性処理の時間計算量について O(n2 ) である．また，る．
（図 17）

全頂点に対してこの処理を行うため扱う問題との相collectExtraNodes(trie, i) は上記の処理を実行する性によらず Ω(n) の時間計算量となる．

関数であり，最大で O(n) 個の頂点に対して最大 O(n)の深さ有限トライ木をさかのぼる．有限トライ木を8 計算量

さかのぼる際には不要な有限トライ木のノードの削提案した差分適用アルゴリズムは各 φ′

(i)

において

除を行い，それには有限トライ木内部の平衡二分木

書換え距離が i 以下であるような頂点についてのみからのエッジの削除を伴うためエッジ数 e に対してcolor (i) を計算し，それによるソートを行うものであO(log e) (≤ O(log n)) の時間がかかる．しかし，有る．また，有限トライ木の各ノードにおいてエッジの

K(7)

F(6)

G(6)

H(6)

I(6)

J(6)

A(5)

B(4)

C(3)

D(2)

E(1)

L(8)

A,B,C,D,E,F

図 19

要素交換に対応するリスト構造の書換え

ただし，点線で表現された辺は削除された辺を表す
図 17

図 14 に対応する有限トライ木に正当性保持のための処理を加えたもの

K(7)

図 18

2

F(6)

G(6)

H(6)

I(6)

J(6)

A(5)

B(4)

C(3)

D(2)

E(1)

L(8)

1

1

2

3

4

1

1

3

4

5

図 20

5

図 19 の書換えにおける書換え距離

彩色グラフによる長さ 5 のリスト構造の表現

ただし，A(1) とは頂点 A が彩色 1 であることを表す

管理を平衡二分探索木で行っていることにより，ソー

E

D

C

B

トはバイナリサーチの形式で行うことができる．した

A

J

K

I

H

G

L

F

がって，各 i における書換え距離 i 以下なる頂点の個数が少ないほど，この提案アルゴリズムは効果を発揮

図 21

図 18 に対応する有限トライ木

する．
提案アルゴリズムの時間計算量を検証することとな

8. 1 バブルソートモデルの表現

る．また，各書換えについて彩色グラフの頂点の削除

ここで例題としてバブルソートの彩色グラフによおよび追加はなく彩色の変化もないため書換え距離 0

る表現に対して，提案アルゴリズムの時間計算量を考の頂点は発生せず，交換を受けた要素を表す頂点およえる．

びその要素を保持するノードを表す頂点が書換え距

バブルソートはリスト構造により保持された 1, ..., n

離 1 となる．
（図 20）の逆順に対して行うものとし，n 個のリスト構造の

なお，差分適用アルゴリズムに関して最初の一つノードを表す頂点（次数 3，彩色 n + 1），1 個のリス

目の彩色グラフに対する初回安定細分化は，頂点数 0

ト構造の先頭を表す頂点（次数 1，彩色 n + 2），1 個のグラフから書換えにより一つ目のグラフが生じたのリスト構造の末尾を表す頂点（次数 1，彩色 n + 3），とみなしアルゴリズムを適用するものとする．

n 個のリスト構造により保持される整数を表す頂点

ここでリスト構造は線形に接続された構造である（次数 1，整数 i を表す頂点について彩色 i）の合計

ため先頭部分からの走査により時間計算量 O(n) での2n + 2 個の頂点と n + 3 色の彩色からなる彩色グラ

一意バイト列生成が可能であるが，本論文で提案する

フによりリスト構造の状態を表現する．
（図 18）このアルゴリズムにおいては構造の線形性を前提にした表現形式においては初回安定細分化により彩色は離ものではなく一般的なグラフ構造に対しても適用可

散的となる．

能なものである．

また，グラフの書換えはバブルソートにおける要素の交換一回に対応させる．
（ 図 19）そ の た め

n(n − 1)/2 + 1 = O(n2 ) 個の彩色グラフ列に対する

8. 2 バブルソートモデルの安定細分化計算量

表 10以降，長さ n のリストにおけるバブルソートの議

表 9 における φ(1) 生成時の各 N i の D(N i )細分化論において，N i によりリスト構造のノードに対応した頂点を，I i により要素である整数に対応した頂点

D(N )
1

を表すものとする．ただし，1 ≤ i ≤ n である．また，

I i は整数 n + 1 − i に対応するものとする．すなわちD(N 2 )..
.

I i の初期彩色は n + 1 − i である．さらに，リストの先頭に対応する頂点は H とし，末尾に対応する頂点
は T とする．なお，初期状態において I i は N i によ1

2

り保持され，先頭から順に N , N , ..., Nn

D(N i )..
.

と接続されているものとする．

8. 2. 1 通常処理における計算量(0)

バブルソート進行の各段階において，φD(N n−1 )においてリスト構造のノードに対応する頂点以外はすべて一元彩色クラスとなり，φ(1)

D(N n )

彩色n−1 個z }| {(0, 0, ..., 0, 1, 1, 1, 0)n−2 個z }| {(0, 0, ..., 0, 1, 0, 2, 0, 0)
..
.
n−i 個
i−1 個
z }| { z }| {(0, 0, ..., 0, 1, 0, 0, ..., 0, 2, 0, 0)
..
.
n−2 個
z }| {(0, 1, 0, 0, ..., 0, 2, 0, 0)n−1 個z }| {(1, 0, 0, ..., 0, 1, 0, 1)

においてリスト構造に対応する頂点がすべて一元彩色クラスとなる．
（表 9）

8. 2. 2 差分適用処理における計算量
バブルソートの初期状態に対応するグラフ構造に

表9

長さ n のリスト構造初期状態における通常の

McKay のグラフ正規化アルゴリズムによる初回安定細分

ついて，すべての頂点の書換え距離は 0 である．また，計算中のグラフ構造を X2 とし，X1 は空なグラ
フとする．

化の進行

細分化

彩色

初期値の設定において，V(X1 ) \ V(X2 ) は空集φ(0)(I n |I n−1 |...|I 1 |N 1 , N 2 , ..., N n |H|T )合であるので trie.delete(v ) は実行されない．また，

φ(1)(I n |I n−1 |...|I 1 |N n |N n−1 |...|N 1 |H|T )trie.root.vertexes = halfwayVertexes = V(X2 ) で
ある．

φ′
(0)

(0)

の 計 算 を 考 え る と ，計 算 開 始 時 にによるソートは彩色の値によるバケットソー

は reverseStack は 空 で あ り，halfwayVertexes =トにより可能である．このとき，時間計算量は頂点数

V(X2 ) で あ る ．halfwayVertexes の 各 元 に つ い て

φに比例するため Θ(n) である．

notLeaf (v .owner ) も し く は notSingleton(v .owner

さらに，φ(1) は D の比較により行われるため，基.vertexes) で あ る の で ，getColor (v , 0 ) と v .owner

数ソートにより可能である．D の生成のために必要な.child [color ].vertexes.push(v ) お よ び nextHalfway

時間計算量は辺の個数に比例するため |E| = 2n + 1

Vertexes.push(v ) が行われる．getColor (v , 0 ) は初期から Θ(n) である．また，基数ソートに必要な時間

彩色を参照すればよいので必要な時間計算量は Θ(1)

計算量はキーの桁数 n + 3 と一元彩色クラスでないである．また，v .owner .child [color ].vertexes.push(v )彩色クラス N 1 , N 2 , ..., N n の大きさ n から Θ(n2 ) ではラベル color を持つエッジによる子ノードに v をある．

渡す処理であるが，有限トライ木のノード v .owner

したがって，グラフ構造一つあたりの安定細分化生
2

成の時間計算量は Θ(n ) である．ゆえにバブルソー
2

ト終了までの状態に対応した Θ(n ) 個のグラフ構造
4が管理する平衡二分木内での挿入操作に等しいため，
彩色数 n + 3 より必要な時間計算量は Θ(logn) である．さらに，halfwayVertexes.push(v ) はスタックへの安定細分化の生成の時間計算量は Θ(n ) であり，グのプッシュ操作であるので Θ(1) である．以上より頂

ラフ構造一つあたりのならし計算量は Θ(n2 ) である．

点ひとつあたりの時間計算量は Θ(log n) であるので，

頂点数 2n + 2 より全体の時間計算量は Θ(n log n) とは空であり，halfwayVertexes も空である．したがっなる．

て時間計算量は Θ(1) となる．

φ′

(1)

の 計 算 を 考 え る と ，計 算 開 始 時 に

φ′

(1)

の計算において，計算開始時に要素交換されたは reverseStack は 空 で あ り，halfwayVertexes =頂点について reverseStack = {I i , I j , N k , N l } であV(X2 ) で あ る ．halfwayVertexes の 各 元 に つる．v = I i , I j に対しては tmpNode.depth = 1 より処

い て ，v が リ ス ト 構 造 の ノ ー ド に 対 応 す

理を行わず，v = I i , I j に対しては tmpNode.depth =る 頂 点 で な い 場 合 ，¬notLeaf (v .owner ) ま た

2 であるので，tmpNode.delete() を一回ずつ行う．しは notSingleton(v .owner .vertexes) で あ る ．v がたがって reverseStack の元に関する処理全体に必要

リスト構造のノードに対応する頂点の場

な時間計算量は Θ(log n) である．

合，notLeaf (v .owner ) または notSingleton(v .owner

こ の と き halfwayVertexes= {N k , N j } で あ.vertexes) で あ る の で ，getColor (v , 1 ) と v .owner

る．{N k , N j } の各元について，notLeaf (v .owner ).child [color ].vertexes.push(v ) お よ び nextHalfway

ま た は notSingleton(v .owner .vertexes) で あ り，Vertexes .push(v ) が 行 わ れ る ．getColor (v , 1 ) は¬(isExistChild (v .owner , color )) または３つの隣接する頂点の color (0) を参照して計算す¬(isLeaf (v .owner .child [color ])) から，getColor (v , 1 )ればよく必要な時間計算量は Θ(1) である．また，と v .owner .child [color ].vertexes.push(v ) および

v .owner .child [color ].vertexes.push(v ) はプレフィッ

nextHalfwayVertexes.push(v ) が行われる．

(1 )における彩色数 n

getColor (v , 1 ) はバブルソートの初期状態と同様

より必要な時間計算量は Θ(log n) である．さらに，に３つの隣接する頂点の color (0) を参照して計算す

halfwayVertexes.push(v ) は Θ(1) である．以上よりればよく必要な時間計算量は Θ(1) である．また，

リスト構造のノードに対応しない頂点ひとつあたり

v .owner .child [color ].vertexes.push(v ) はプレフィッの時間計算量は Θ(1) であり，リスト構造のノードにクスを共有する頂点の color (1) における彩色数 n よ対応する頂点ひとつあたりの時間計算量は Θ(log n)

り必要な時間計算量は Θ(log n) である．さらに，である．ゆえに，全体の時間計算量は Θ(n log n) とhalfwayVertexes.push(v ) は Θ(1) である．以上よりなる．

{N k , N j } の各元での時間計算量は Θ(log n) である．

クスを共有する頂点の color

したがって，バブルソートにおける初期状態を表現するグラフ構造の初回安定細分化に必要な時間計算量は Θ(n log n) である．
′ (i)ここで，各 φの計算において本来の McKay の以上より，全体の時間計算量は Θ(log n) となる．
以上より，バブルソートにおける要素交換で得られた状態を表現するグラフ構造の初回安定細分化に必
要な時間計算量は Θ(log n) である．

グラフ正規化アルゴリズムの細分化での長さ Θ(n) のしたがって，バブルソート終了までの状態に対応しベクトルの辞書式な比較の代わりにハッシュ値を用いた Θ(n2 ) 個のグラフ構造の安定細分化の生成の時間計

た比較が行われることで差分を適用せずとも計算量

算量は初期状態にかかる Θ(n log n) とのこりの Θ(n2 )の改善が起きていることがわかる．

個のそれぞれにかかる Θ(log n) から Θ(n2 log n) で次に，バブルソートにおける要素交換処理によって得られる状態に対応するグラフ構造について，得られある．ゆえに，グラフ構造一つあたりのならし計算量は Θ(log n) である．

たグラフを X2 ，要素交換前の状態に対応するグラフ
を X1 とする．

8. 3 バイト列生成の計算量

初期値の設定において，V(X1 ) \ V(X2 ) は空集

バブルソートのモデルについて，通常の McKay の合であるので trie.delete(v ) は実行されない．また，

グラフ正規化アルゴリズムにおけるグラフ一つあた

trie.root.vertexes = halfwayVertexes = ∅ である．

りの初回安定細分化のならし計算量は Θ(n2 ) であり，

′ (0)

φ

の計算において，計算開始時に reverseStack

差分適用におけるグラフ一つあたりのならし計算量は Θ(log n) である．

るような問題におけるバイト列生成の計算量の改善，

しかし，得られた有限トライ木からバイト列の生成

有限トライ木のコピーの計算量の改善などが課題であを行う際には，有限トライ木の表現する彩色を得てそる．さらにグラフ書換え系に記述された書換え規則のれを基に隣接行列や隣接リストをバイト列に変換す解析による最適なバイト列の文法の生成も検討する．

ることとなるためそれらの分の時間計算量が必要と謝辞

なる．彩色の計算は有限トライ木の深さ優先探索に

本研究を行うにあたり，貴重な意見を頂いた上より可能であり，バブルソートの場合には Θ(n) であ田研究室 LMNtal 班の皆様に感謝いたします．まる．また，リスト構造を表現するグラフについて辺数

た，本研究の一部は， 科学研究費補助金 (基盤研究は n に比例するので隣接リストによる表現の長さも(B)23300011) の補助を得て行った．

n に比例し，バイト列の生成は Θ(n) で可能である．
したがって，バブルソートにおいての初回安定細分化

参 考 文 献処理のあとに行うバイト列生成のための処理は Θ(n)[1] Hartke, S. G. and Radcliﬀe, A. : McKay’s
Canonical Graph Labeling Algorithm, Communicating Mathematics, 479 Contemporary Mathematics, American Mathematical Society, 2009,
pp. 99–111.
[2] Hedrlin, Z. and Pultr, A. : On full embeddingsof categories of algebras, Illinois Journal of Mathematics 10 (3), 1966, pp. 392–406.
[3] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal, コンピュータソフトウェア 25 (1),2008, pp. 124–150.
[4] McKay, B. D. : Practical Graph Isomorphism,
Congr. Numer 30, 1981, pp. 45–87.
[5] Miller, G. L. : Graph Isomorphism, General Remarks, J. Comput. System Sci 18, 1979, pp. 128–
142.
[6] Milner, R. : The Space and Motion of Communicating Agents, Cambridge University Press, 2009.
[7] Miyazaki, T. : The complexity of McKay’s canonical labeling algorithm, Groups and Computation,
II (New Brunswick, NJ, 1995), DIMACS Ser. Discrete Math. Theoret. Comput. Sci., 28. Amer.
Math. Soc,. Providence, RI, 1997, pp. 239–256.
[8] Rensink, A. : The GROOVE Simulator: A Tool
for State Space Generation, Applications of Graph
Transformations with Industrial Relevance, LNCS
3062, Springer-Verlag, 2004, pp. 479–485.

の時間計算量であり，初回安定細分化に対応した有限トライ木を得るための時間計算量が Θ(log n) である
バブルソートのモデルにおいてはボトルネックとな
りうる．しかし，バイト列生成の計算量を含めても差分適用による時間計算量 Θ(n) は差分不適用の Θ(n2 )よりも小さなオーダである．

9 まとめと今後の課題
本論文では，彩色単純グラフにおける一意バイト列
生成手法に用いられる McKay のグラフ正規化アルゴ
リズムにおけるグラフ構造の差分情報を活用することによる最適化手法を考案した． このグラフ構造の一意バイト列生成の高速化によりグラフ書換え系をモデリング言語としたモデル検査の処理時間を改善することができる．
なお，実際のモデル検査においては状態遷移が枝分かれするようなモデルが存在し，そのような際には今回の差分適用アルゴリズムを実現するためには生成した有限トライ木のコピーの処理が必要であり，それには有限トライ木のノード数に比例した時間計

A 付録: 証明算量が必要となる．バブルソートモデルの場合に有限定理 4.1 の証明

トライ木のコピーを考えると Θ(n) であり，バイト列生成と同様にボトルネックとなりうる．
今後は，本アルゴリズムを実装しグラフ書換え系の証明 A.1 k = 0 において

EC0 = φ = φ(0) より命題は成立する．
また，k において命題が成立すると仮定して，処理系に組み込むことで，実際のモデル検査におけるφ(k+1) (v) = φ(k+1) (w) は定義から性能を計測する．また，アルゴリズムに使用している

D(v) = (φ(k) (v), d1 (v), d2 (v), ..., dl (v)) より

ハッシュ値の衝突率のモデル検査における振る舞いや

φ(k) (v) = φ(k) (w),

初回安定細分化処理の時間計算量が線形オーダを下回

(0)

(0)

d1 (v) = d1 (w),

φ2 (w2 ) = φ2 (w2 ) = φ1 (w1 ) = φ1 (w1 )d2 (v) = d2 (w),..
.

より成立する．

dl (v) = dl (w)D(v2 ) = (φ(i) (v2 ), d1 (v2 ), d2 (v2 ), ..., dn (v2 ))また，i において命題が成立すると仮定すると，

D(w2 ) = (φ(i) (w2 ), d1 (w2 ), d2 (w2 ), ..., dn (w2 ))に等しい．

di (v) は v の φ(k)での彩色 i をもつ隣接頂点の重複度に等しいので，の辞書式な比較により φ(i+1) (v2 ) と φ(i+1) (w2 ) の間の大小関係が定まる．

上記はφ(i) (v1 ) < φ(i) (w1 ) の場合，

φ(k) (v) = φ(k) (w)φ(i) (v2 ) < φ(i) (w2 ) より φ(i+1) (v2 ) < φ(i+1) (w2 )

かつ

である．

{|ECk (u) | u ∈ adj(v)|} = {|ECk (u) | u ∈φ(i) (v1 ) = φ(i) (w1 ) の場合，
D(v1 ) = (φ(i) (v1 ), d1 (v1 ), d2 (v1 ), ..., dm (v1 ))adj(w)|}

D(w1 ) = (φ(i) (w1 ), d1 (w1 ), d2 (w1 ), ..., dm (w1 ))

に等しい．
すなわち，

ECk+1 (v)とおく．

=

ECk+1 (w)

⇔

φ

(k+1)

(v)

=

φ(k+1) (w)(d1 (v2 ), d2 (v2 ), ..., dn (v2 )) と(d1 (w2 ), d2 (w2 ), ..., dn (w2 )) においてである．

ともに値が 0 であるような dk を取り除き，新たに

以上より k に関する数学的帰納法により示された．

2

番号を振り直したものを，(d1 (v2 ), d2 (v2 ), ..., dn′ (v2 )) と(d1 (w2 ), d2 (w2 ), ..., dn′ (w2 )) とすると，定理 4.2 の証明

これらは証明 A.2 r < n により安定細分化 φ = φ(r) が得ら{|φ2 (u) | u ∈ adj(v2 )|} + {|φ2 (u) | u ∈ adj(w2 )|}れる．

に小さい順に 1 から n′ まで順に彩色を対応させ直このとき，m ≥ n について

(i)

(i)

したものに等しい，

EC∞ (v) = EC∞ (w)また，⇔ ECn (v) = ECn (w)(d1 (v1 ), d2 (v1 ), ..., dm (v1 ))⇔ φ(n) (v) = φ(n) (w)(d1 (w1 ), d2 (w1 ), ..., dm (w1 ))

⇔φ

(r)

についても同様に

⇔φ

(m)

(r)

(v) = φ(v) = φ

(w)

(m)

(w)

(d1 (v1 ), d2 (v1 ), ..., dm′ (v1 ))⇔ ECm (v) = ECm (w) 2(d1 (w1 ), d2 (w1 ), ..., dm′ (w1 ))とでき，彩色の再対応付けを考えることができる．

定理 4.3 の証明

ここで，証明 A.3 (Si (v1 ), φ1 ) ∼= (Si (v2 ), φ2 ) における同型
写像を g とし，(Si (w1 ), φ1 ) ∼= (Si (w2 ), φ2 ) における同型写像を h とする．

v1g = v2 , w1h = w2 であるので，φ2 (v2 ) = φg1 (v2 ) =φ1 (v2g−1) = φ1 (v1 ) か つ φ2 (w2 ) = φh1 (w2 ) =−1

φ1 (w2h) = φ1 (w1 ) となる．

1

adj(w1 )h = adj(w2 ) であり，u1 ∈ adj(w1 ) について (Si (u1 ), φ1 ) ∼= (Si (uh1 ), φ2 ) である．
したがって，(i)(i){|φ1 (u) | u ∈ adj(v1 )|} + {|φ1 (u) | u ∈ adj(w1 )|}i = 0 のとき，(0)adj(v1 )g = adj(v2 ) であり，u1 ∈ adj(v1 ) についてg
(Si (u1 ), φ1 ) ∼= (Si (u ), φ2 ) であり，の順序構造は(0)

φ2 (v2 ) = φ2 (v2 ) = φ1 (v1 ) = φ1 (v1 )

(i)

(i)

{|φ2 (u) | u ∈ adj(v2 )|} + {|φ2 (u) | u ∈ adj(w2 )|}= (d1 (v2 ), d2 (v2 ), ..., dn′ (v2 ))(d1 (w1 ), d2 (w1 ), ..., dm′ (w1 ))の順序構造に等しい．
ただし，ここで多重集合の加法で得られるものは各= (d1 (w2 ), d2 (w2 ), ..., dn′ (w2 ))多重集合の要素数を合わせたものを要素数とする多であるので，命題は成立する．

重集合である．

以上より i に関する数学的帰納法により示された．

以上より，(d1 (v1 ), d2 (v1 ), ..., dm′ (v1 ))2