ブール関数と組合せ集合の圏論的性質に基づくBDDとZDDの比較

ブール関数と組合せ集合の圏論的性質に基づく

BDD

と

ZDD

の比較

Comparing BDDs and ZDDs via Categorical Properties of

Boolean Functions and Combination Sets

小島 健介

1∗

Kensuke Kojima

1

1

_{京都大学大学院情報学研究科}

1

_{Graduate School of Informatics, Kyoto University}

Abstract: We investigate how binary decision diagrams (BDDs) and zero-suppressed BDDs (ZDDs) differ from each other from a conceptual aspect, aiming to spot the fundamental charac-teristics that distinguish the two data structures. A BDD and a ZDD can represent both a Boolean function and a combination set (a set of sets). However, we argue that it is more natural to regard a BDD as a representation of Boolean functions, and a ZDD as that of a combination set. We for-mally state and prove this on the basis of the observation that Boolean functions and combination sets are equipped with different structures from a category-theoretic point of view. The difference can be captured by using the notion of functors. The functor structures of Boolean functions and combination sets are reflected precisely in the definitions of BDDs and ZDDs, respectively, and this fact can be formally described by using the notion of natural transformations. In addition, we discuss analogous results for sequential decision diagrams, one of the variants of BDDs.

1

はじめに

本稿では，二分決定グラフ (Binary Decision Tree;

BDD) [8, 1] とゼロサプレス型二分決定グラフ (Zero-Suppressed BDD; ZDD) [9, 12] という二つのデータ構 造の違いを考察する．詳しくは 2 節で解説するが，これ らはいずれも組合せ集合あるいはブール関数を表現する データ構造である．組合せ集合とブール関数の間には一 対一の対応があるので，その対応のもとで，BDD/ZDD はいずれの表現ともみることができる．しかし，BDD はブール関数の表現とみたほうが自然であり，ZDD は 組合せ集合の表現とみたほうが自然である．本稿では， このことを数学的な定理として定式化し，証明する． 定式化の概要は次の通りである．まず，ブール関数 と組合せ集合の違いを数学的に定式化する．両者の間 には一対一の対応があるが，ある種の構造（本稿では それを関数の作用と呼ぶ）まで考えれば両者は本質的 に異なっていることがわかる．この構造を備えている 数学的対象は関手と呼ばれる．次に，その構造の違い が BDD/ZDD のデータ構造の定義に反映されているこ とを示す．このことは，関手の間の自然変換の概念を ∗_{連絡先： 京都大学大学院情報学研究科}        〒 606-8501 京都市左京区吉田本町        E-mail: [email protected] 用いて記述できる．また，この結果は BDD/ZDD に限 定されるものではなく，それらの拡張である SDD と ZSDD に対しても同様のことが成立する． 本稿の構成は以下の通りである．まず 2 節で，BDD と ZDD，およびそれらのブール関数と組合せ集合と しての解釈を定義する．続いて 3 節で，関手と自然変 換の定義を述べ，BDD/ZDD の解釈が自然変換になっ ていることを示す．ここまでの議論では，話を簡単に するため，通常の BDD/ZDD で考慮される要素間の 順序は考えない．4 節では，要素間の順序を考慮した 場合にも類似の結果が成り立つことを説明する．また， SDD/ZSDD に対しても同様の考察を行う．最後に 5 節 で本稿のまとめを述べる．

2

二分決定グラフ

2.1

組合せ集合とブール関数

集合 X の部分集合のことを X 上の組合せ (combina-tion) といい，X 上の組合せの集合のことを，X 上の組 合せ集合 (combination set) という．本稿では X のこ とを全体集合と呼ぶことがある．例えば，全体集合 X として有向グラフ G の辺全体の集合を考えてみよう． 人工知能学会研究会資料 SIG-FPAI-B509-10

G の全域部分木やハミルトン閉路は，G の辺の集合と して表現できるから，X 上の組合せとみなせる．した がって，全域部分木全体やハミルトン閉路全体の集合 は組合せ集合（と同一視できる集合）の例である． X 上の組合せ集合全体の集合を CS (X) と書く．混 乱のおそれがないときは，組合せをその要素の列で表 す．例えば，_{{{a}, {b}, {a, b}} の代わりに {a, b, ab} と}

書く．また，_{∅ は組合せでも組合せ集合でもあるが，こ} れを組合せとみているときは ε と書いて区別する． 集合 X 上のブール関数 (Boolean function) とは，X の要素への真理値の割り当て（X から{0, 1} への関数） を受け取って 0 または 1 を返す関数のことである．X 上のブール関数全体の集合を BF (X) と書く．ブール関 数は X が有限集合であれば論理式で表現できる1_．例 えば a∨ b は，a と b の少なくとも一方に 1 が割り当て られていれば 1 を，そうでなければ 0 を返すブール関 数を表現する．以下，ブール関数と論理式は混乱のお それがない限り特に断りなく同一視する． 組合せ集合とブール関数の間に一対一の対応がある ことはよく知られている．例えば，上で挙げた_{{a, b, ab}} とブール関数 a∨ b は互いに対応している．一般に，次 のことが成り立つ． 命題 1. 組合せ集合 P ∈ CS(X) に対してブール関数 τX(P )∈ BF (X) を，各真理値割り当て ρ: X → {0, 1} に対して τX(P )(ρ) = 1 ⇐⇒ ρ−1(1)∈ P となるよう に定義する．このとき，τXは CS (X) から BF (X) へ の全単射である．

2.2

BDD と ZDD の定義

BDD と ZDD は，組合せ集合（あるいはブール関数） の有向グラフによる表現である．命題 1 により，ある データを組合せ集合として解釈することとブール関数 として解釈することとは同値である． BDD と ZDD は，単なる有向グラフとしては同じ構 造をしている．そこで本稿ではまず最初に BDD や ZDD になりうる有向グラフ（ダイアグラムと呼ぶことにす る）のクラスを定義し，続いてダイアグラムの BDD および ZDD としての解釈を定義する．このようにし ておいた方が 3 節での定式化の際に都合がよい．なお， BDD/ZDD を考えるときには要素間に順序を導入する のが普通だが，それについては 4.1 節で考察する． 定義 2. 集合 X 上のダイアグラムとは，節点と枝にラ ベルをもつ閉路のない根付き有向グラフで，以下の条 件を満たすものである． 1_{以下，断らなければ有限集合のみを考えることにするが，X が} 無限集合の場合でも，本稿の議論は論理式を用いない形に修正すれ ば成立する． '&%$ !"#a  '&%$ !"#_b = = = = 0 1 図 1: ダイアグラムの例．丸は分岐節点，四角は終端節 点を表し，点線と実線はそれぞれ 0-枝，1-枝を表す．

• 節点は分岐節点 (decision nodes) と終端節点

(ter-minal nodes) の二種類に分けられる． • 分岐節点は X の要素でラベル付けされており，2 本の区別された枝をもつ．これらの枝はそれぞれ 0 と 1 でラベル付けされ，0-枝，1-枝と呼ばれる． • 終端節点は枝をもたず，0 または 1 でラベル付け される（それぞれ 0-終端節点 (0-terminal node)， 1-終端節点 (1-terminal node) と呼ぶ）． X 上のダイアグラム全体の集合をD(X) と書く．ダ イアグラムは通常，図 1 のように図示される． 以下，表記を簡単にするために，0-終端節点と 1-終 端節点をそれぞれ 0 と 1 で表す．また (a, F, G) でラベ ル a をもち 0-枝と 1-枝がそれぞれ F と G を指す分岐 節点を表す．例えば，図 1 のダイアグラムをこの記法 を用いて書き下すと (a, (b, 0, 1), 1) となる．なお，ダイ アグラムをこのように表現すると，節点が共有されて いたかどうかの情報が失われてしまうが，節点の共有 の有無は本稿の議論においては重要ではない． 次に，ダイアグラムをデータ構造として解釈する方 法を与える．これはダイアグラムを受け取ってブール関 数または組合せ集合を返す関数として定義できる．これ らの関数のことを以下では解釈関数と呼ぶことにする． ダイアグラムの BDD としての解釈 β は，ブール関 数を返す次のような関数である． β(0) = false β(1) = true β((a, F, G)) = (¬a ∧ β(F )) ∨ (a ∧ β(G)) 手続き的に説明すると，関数 β(F ) は，真理値割り当 て ρ が与えられたとき次のように動作する．F の根か ら探索を始めて，今見ている分岐節点のラベル x を取 得し，ρ(x) の値が 0 なら 0-枝を，1 なら 1-枝をたどる， という処理を繰り返す．終端節点に到達したら，その 終端節点のラベル（これは 0 または 1 である）を返す． 上の定義の右辺を組合せ集合とみると，終端節点は それぞれ_{∅, P(X) で解釈され，分岐節点 (a, F, G) は} {A ∈ β(F ) | a /∈ A} ∪ {A ∈ β(G) | a ∈ A} で解釈される．例えば図 1 の BDD としての解釈は，定 義から得られる式を同値変形すると a∨ b となることが わかり，これは組合せ集合としては_{{a, b, ab} である．}

一方，ZDD としての解釈 ζ は次のように定義される． ζ(0) =∅ ζ(1) ={ε} ζ((a, F, G)) = ζ(F )∪ {A ∪ {a} | A ∈ ζ(G)} BDD の場合と同様に手続き的に説明すると，次のよう になる．ZDD においては，根から 1-終端節点に至る各 パスが組合せを表す．各分岐節点において，その節点 から 0-枝をたどることは，その節点に付いているラベ ルを選ばないことを意味し，1-枝をたどることは選ぶ ことを意味する．パスが表す組合せは，そのパスに沿っ て要素を選択していったときに最終的に得られる組合 せである．したがって特に，1-終端節点の解釈は{ε}， すなわち何も含まない組合せのみからなる組合せ集合 となる．例えば図 1 を ZDD として解釈すると，{a, b} となる．a と b の両方を選択して 1 に至るパスが存在 しないため，BDD の場合と違って ab は含まれない．

2.3

二つの表現の違い

BDD と ZDD の違いは，ダイアグラム中に（より正 確にはパス中にだが）現れない要素の扱いにある [9, § 2–3]．それは以下のようにまとめることができる． X 上の BDD F に一度も現れない要素 x∈ X があっ たとする．このとき，先に述べた β(F ) の動作に照らし て考えると，F が表すブール関数の値の計算に x への 割り当ては使われない．したがって，x が真と偽のど ちらを割り当てられようと結果には影響しないことが わかる．これは組合せ集合の言葉に直せば，F が表す 組合せ集合にある組合せ C が属するか否かは，x∈ C か x /∈ C かとは無関係に決まるということである． 一方で ZDD においては，選択することを明示的に指 示されたものだけが組合せに入っていると解釈される． したがって，ZDD 中に現れない要素は入らないと解釈 されなければならない．つまり ZDD においては BDD とは違い，x が F に現れないときには x∈ C であるよ うな組合せ C は ζ(F ) に入らない． この違いがどのような差を生むかをみるために，例 として図 1 のダイアグラムを考え，これを F とする． 今までは F を X ={a, b} 上のダイアグラムだと暗に 仮定していたが，そうではなく Y ={a, b, c} 上のダイ アグラムと考えることもできる．いずれの場合でも，F を BDD として解釈して得られるブール関数は論理式 で書くと a∨b になるが，これを組合せ集合だと思うと， 二つの場合で同じ集合にはならない．実際，X 上で考 えれば_{{a, b, ab} だが，Y 上では {a, b, ab, ac, bc, abc} と} なる．また，F を ZDD として解釈すると組合せ集合 {a, b} になるが，これをブール関数だと思っても同様 のことが起きる．すなわち Y 上で{a, b} に対応する論 理式は，X 上で考えたときの論理式と¬c との連言で ある（c を含む組合せを排除するため）．よって同じ組 合せ集合が X 上と Y 上では異なる論理式で表される． このような事情から「BDD は関数の表現，ZDD は集 合の表現」と考えるのが自然であると考えられる．

3

数学的定式化

前節で述べた BDD と ZDD の違いは，ひとことで言 い表すと，全体集合 X をより大きい Y に置き換えたと きの解釈の変化が BDD と ZDD では異なる，というこ とだった．このように「考えている集合が変化するとど うなるか」に注目することが定式化の鍵になる．ダイ アグラムや組合せ集合，ブール関数という概念を，単 に個々の集合 X について定義されているだけでなく， X が変化すればそれに合わせてそれらも何らかのしか たで変化すると考える．上の例では X ⊆ Y の場合に ついて考えたが，より一般に関数 f : X → Y があると （X ⊆ Y は f が X から Y への包含写像になっている 場合である），f に沿ってダイアグラムなどを「変化さ せる」ことができる．本節では，この状況を圏論 [2] の 用語を使って整理する2_．

3.1

関数の作用と関手

集合を作る操作_{F であって，上に述べたような「変} 化」が定まっているものを関手という．正式な定義は 以下の通りである． 定義 3. すべての集合 X に対して何らかの集合F(X) が与えられていて，かつすべての関数 f : X → Y に対し て関数_{F(f): F(X) → F(Y ) が与えられているとする．} このとき_{F が関手 (functor) であるとは，f が恒等写像} ならば_{F(f) も恒等写像であり，かつすべての関数 f, g} について（f◦g が定義できれば）F(f ◦g) = F(f)◦F(g) であることをいう． F(f) のことを，関数 f が集合 F(X) から F(Y ) へ の変換を与えているとみて，f の (F に関する) 作用 (action) と呼ぶことにする [7,§ V.7]．なお集合と関数 のいずれに対する操作も同じ_{F で表すが，どちらを表} すかは文脈から判断できるだろう． 例えば，集合 X に対して List(X) を X の要素の有 限列全体からなる集合とする．このとき，List は関数 f : X → Y に対して List(f) を map f，すなわち List(f )([x1, . . . , xn]) = [f (x1), . . . , f (xn)] と定義することで関手になる．実際，List が関手の条 件を満たしていることは容易に確かめられる． 2_{本稿で与える関手と自然変換の定義は，考えている圏がすべて} 集合と関数の圏の場合のものである．

3.2

自然変換

関手による関数の作用を保存する変換のことを自然 変換という．正式な定義は以下の通りである． 定義 4. F, G を関手とする．すべての集合 X に対し て関数 αX:F(X) → G(X) が与えられているとき，族 α = {αX}X をF から G への変換 (transformation) という．さらに，どんな関数 f : X → Y に対しても G(f) ◦ αX = αY ◦ F(f) が成り立つとき，α は自然変 換 (natural transformation) であるという． いま仮に f の x への作用を f·x と（F(f) と G(f) の区 別がつかなくなることに目をつぶって）表すことにする と，自然変換の条件は_{∀x ∈ F(X), f ·α}X(x) = αY(f·x) と書ける．このように表現すれば，この条件が作用の 保存を表していることが見て取れるだろう． より直観的には，自然変換とは_{F や G の形のみに} 依存し，それ以上の余分な情報によらない関数である． 例として_{F = G = List のときを考える．受け取った} リストを逆順にして返す関数は，リストの構造を変更 するだけで，リストの要素が何であるかには依存しな い．大雑把にいって，このような関数が自然変換であ る．一方，リスト中の重複する要素を削除する関数は， リストに何が入っているかによって何番目の要素が削 除されるかが異なる．すなわちリストの具体的な要素 という「余分な情報」に依存して，返されるリストの 構造が変わる．こういう関数は自然変換にはならない． 実は，この「余分な情報によらない関数」であること が，自然変換の定義が本来意図するところである．も ともと自然変換は，例えばベクトル空間の間のある線 形写像の作り方が基底のとり方に依存するかしないか， というような違いを表すために導入された概念である [5, 6]．基底のとり方に依存しない線形写像は自然であ り，依存するものは自然ではない，というような言葉 遣いは自然変換という概念が生まれる前から使われて いた．基底はベクトル空間の構造（適当な条件を満た す加法とスカラー倍）そのものに内在するわけではな く，同じベクトル空間に対していろいろな基底がある から，その意味で基底は「ベクトル空間一般」を考え ている際には余分な情報である．そういう余分な情報 を使わないで定義できる対象が「自然である」とされ る．そのような「自然さ」の直観とうまく一致しそう な概念として導入されたのが，自然変換である．現在 では，上の定義がより直観的な意味での自然さと比較 的よく一致するものとして受け入れられている．

3.3

解釈関数の自然さ

次に BDD/ZDD の解釈関数が自然変換になっている ことを示す．その前に，ダイアグラムや組合せ集合な どの構成を関手に拡張する（すなわち関数の作用を定 義する）必要があるが，これは難しくない． まずダイアグラムの関手_{D を作る．D(X) はすでに} 定義した通り，集合 X 上のダイアグラムの集合である． 関数 f : X→ Y に対して，その作用 D(f) はラベルの 付け替えである（これは List が定める作用が map だっ たことの類似である）．正確には D(f)(0) = 0, D(f)(1) = 1, D(f)((a, F, G)) = (f(a), D(f)(F ), D(f)(G)) と書ける．これが関手の条件を満たすことは容易に確 かめられる． 次にブール関数と組合せ集合の関手 BF , CS を定義 する．関数 f : X → Y の作用を BF (f )(φ(x1, . . . , xn)) = φ(f (x1), . . . , f (xn)), CS (f )(P ) ={f(A) | A ∈ P } と定める．ただし φ(x1, . . . , xn) は X 上のブール関数 を論理式で表したものであり，x1, . . . , xn ∈ X である （φ の選び方はいくつもあるが，右辺はブール関数とし ては φ の選び方によらずに定まる）．これらの定義が 関手を定めることも容易に確認できる． 以上の準備のもとで，本稿の主定理は以下のように 述べることができる． 定理 5. 1. β はD から BF への自然変換である． 2. ζ はD から CS への自然変換である． Proof. 任意のダイアグラム F について BF (f )(β(F )) = β(D(f)(F )) および CS(f)(ζ(F )) = ζ(D(f)(F )) が成り 立つことを示せばよい．これらは F の節点数について の帰納法で証明できる． ブール関数と組合せ集合が本質的に異なる数学的対 象であることの証拠として，次の命題が成り立つ． 命題 6. BF (X) と CS (X) は，同型だが自然には同型で ない．すなわち，各 X に対して全単射 αX: BF (X)→ CS (X) があるが，この全単射を α が自然変換になるよ うに構成することはできない． この命題の証明は省略するが，例えば，命題 1 で与 えた対応 τ はが自然変換ではないことは容易に確かめ られる．X を空でない集合，i : ∅ → X を包含写像と すると，BF (i)◦ τ∅ ̸= τX◦ CS(i) である（両者は {ε} をそれぞれ true と∧_x∈X(¬x) に写す）． なお，τ−1_{◦ β は D から CS への変換であるが，これ} は自然変換にはならない．同様に τ◦ζ も D から BF へ の自然ではない変換である．実はより強く，どんな全 単射な変換 α : BF → CS を用いても，変換 α−1_{◦ β と}

α◦ ζ は自然にはできないことが示せる．このことは， BDD を組合せ集合として解釈する，あるいは ZDD を ブール関数として解釈するのが自然ではないことを意 味していると考えられる．これを前節の自然さの意味 付け沿ってより直観的に理解するなら，次のようにな るだろう．1 の解釈に注目する．1 には X の情報は含 まれていないが，もしこれを BDD とみたうえで組合 せ集合として解釈すれば，結果は_{P(X) となり，X が} 何であるかに依存する．また，1 を ZDD とみると解釈 は_{{ε} になるが，これはブール関数として表現しよう} とすれば∧_x∈X(¬x) のようになり，やはり X が何であ るかに依存する．このような，ダイアグラムには現れ ないにもかかわらず考慮しなければならない要素の情 報が，「余分な情報」にあたると考えられそうである．

4

いくつかの拡張

4.1

要素間の順序を考慮した BDD/ZDD

これまでは全体集合 X には何の構造も仮定しなかっ たが，実際に BDD や ZDD を扱う際は，あらかじめ要 素間に順序を導入しておき，その順序に従って要素が出 現するようなグラフを考える [3]（そのような BDD を 特に ordered BDD (OBDD) と呼ぶこともある）．その ような制約を考慮しても，ダイアグラムの解釈は 3 節 と同様に自然であることが示せる．ただし，その主張 内容を正しく述べるには，関手と自然変換の定義を少 し変更する必要がある3_{．その概要は次のとおりである．} (X,≤) を全順序集合とする．X 上のダイアグラム F が_{≤ と整合するとは，F において y が x の子孫として} 現れるならば x < y であることとする．D′_{(X,≤) を ≤} と整合する X 上のダイアグラム全体の集合とする．こ のとき_D′は以前と同様の作用で関手になるが，作用さ せる関数は任意の関数ではなく，狭義単調なものに限 らなければならない．もし F ∈ D′_{(X,≤) に狭義単調} でない関数 f : X→ Y を作用させると，得られるダイ アグラムは Y の順序と整合するとは限らないからであ る．これに合わせて，自然変換の定義も，「すべての狭 義単調な関数について作用が保存されること」と変更 する．以上の修正を施すと，定理 5 と同様の主張がD′ について証明できる．

4.2

Sentential Decision Diagrams

ここまでは BDD と ZDD の対比を見てきたが，両 者の拡張である sentential decision diagram (SDD) [4] と zero-suppressed SDD (ZSDD) [10] に対しても同様 のことがいえる．本節ではその概要を説明する． 3_{関手の定義域を全順序集合と狭義単調関数の圏に変えなければ} ならない． 定義 7. 集合 X が与えられたとき，その上の SDD α とそのブール関数としての解釈 σ(α)∈ BF (X) は以下 のように定義される4_． • ⊤ と ⊥ は SDD であり，その解釈はそれぞれ true と false である． • x ∈ X に対して，x と ¬x は SDD であり，その 解釈はそれぞれブール関数としての x と¬x で ある． • pi, siが 1 ≤ i ≤ n に対して SDD であるとき， {(p1, s1), . . . , (pn, sn)} は SDD であり，その解釈 は∨n_i=1(σ(pi)∧ σ(si)) である． 定義 8. 集合 X が与えられたときに，その上の ZSDD α とその組合せ集合としての解釈 ξ(α) は以下のように 定義される． • ⊤ と ε は ZSDD であり，その解釈はそれぞれ {ε} と_{∅ である．} • x ∈ X に対して，x と ±x は ZSDD であり，そ の解釈はそれぞれ_{{{x}} および {ε, {x}} である．} • pi, siが 1≤ i ≤ n に対して ZSDD であるとき， {(p1, s1), . . . , (pn, sn)} は ZSDD であり，その解 釈は∪n i=1(ξ(pi)⊔ ξ(si)) である．ただし⊔ は次 のように定義される演算である: P⊔ Q = {A ∪ B | A ∈ P, B ∈ Q}. 上で定義された解釈について，前節の定理 5 と同様 の以下の定理が成り立つ．証明は，CS (f ) が∪と_{⊔ を} 保つことに注意すればできる． 定理 9. 1. SDD (X)，ZSDD (X) をそれぞれ X 上 の SDD, ZSDD の集合とすると，SDD と ZSDD はラベルの付け替えを作用として関手になる． 2. σ は SDD から BF への自然変換である． 3. ξ は ZSDD から CS への自然変換である． SDD と ZSDD についても 4.1 節と同様の議論ができ る．上の議論中に現れる順序を vtree [11] に置き換え て適切に定義を変更すればよい．Vtree とは，集合の 分割のしかたを表す二分木で，次のように定義される． 定義 10. 集合 X の vtree とは，根付き完全二分木で あって，その葉の集合と X との間に一対一の対応が与 えられているもののことである． 4_{本来は vtree と呼ばれる木の構造を考慮して定義するが，これ} については後ほど考察する．また，piが分割 (partition) になると いう条件が本来は付くが，本稿ではこの条件は外して考える．

以下，x∈ X と対応付けられる葉を単に x，左右の 子がそれぞれ v, w である vtree を (v, w) と書く． v, w を vtree とし，その葉に対応する要素の集合 （定義 10 の X）をそれぞれ|v|, |w| と書くとき，関数 f :|v| → |w| が v から w への埋め込みであることを次 のように再帰的に定義する． • v が葉なら f は埋め込みである． • v = (v1, v2), w = (w1, w2) であって，f は|vi| に 制限すると vi から wiへの埋め込みになる (i = 1, 2) なら，f は v から w への埋め込みである． Vtree との整合性を次のように定義する（SDD と ZSDD で定義はほぼ同じなので，まとめて定義する）． • ⊤, ⊥, ε は任意の vtree と整合する． • x, ¬x, ±x は x ∈ |v| となる任意の v と整合する． • {(p1, s1), . . . , (pn, sn)} は，各 piが v と，各 siが w と整合するとき，(v, w) と整合する． この定義は “α respects v” [4, Def. 5] の定義と似て いるが，二番目の規則が異なる．このように定義する と，vtree の埋め込み f に対し，先ほど定義した f の SDD/ZSDD への作用は整合性を保つ．この作用を用 いれば，vtree v に対してそれと整合する SDD の全体 SDD′(v) をとる関手が定義できる5_{．自然変換の定義を} vtree の埋め込みによる作用を保存することと変更す れば，SDD の解釈関数 σ は SDD′から BF（正確には BF◦ | · |）への自然変換になることが示せる．また ξ に ついても，ZSDD′を同様に定義すれば，ZSDD′ から CS への自然変換であることが示せる． なお上の埋め込みの定義によると，例えば (a, b) を (c, (a, b)) に（ラベルを変えずに）埋め込むことはでき ないが，これは許されてもよさそうに思われる．それ が可能になるように埋め込みの定義を拡張することは できるが，そのように拡張した場合にも同様の結果が 成立するかどうかは本稿の執筆時点では未確認である．

5

おわりに

本稿では，ブール関数と組合せ集合の持つ圏論的な 構造の違いに注目することで，BDD はブール関数の表 現であり ZDD は組合せ集合の表現であるということ を数学的な定理として定式化できることを示した．ま た，若干の修正のもとで同様の議論が SDD/ZSDD に 対しても成立することを示した．このことから，本稿 で提示したブール関数と組合せ集合の区別，およびそ れに基づくデータ構造の性質の違いの定式化は，一定 の普遍性を備えているものであると予想される． 5_{正確には，SDD}′_{の定義域は vtree と埋め込みのなす圏である．} ZSDD′も同様．

謝辞

本研究は CREST, JST, JPMJCR1401 の支援を受け たものです．

参考文献

[1] Sheldon B. Akers. Binary decision diagrams.

IEEE Trans. Comput., Vol. C-27, No. 6, pp. 509–

516, 1978.

[2] Steve Awodey. Category Theory. Oxford Univer-sity Press, 2010.

[3] Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., Vol. 35, No. 8, pp. 677–691, 1986.

[4] Adnan Darwiche. SDD: A new canonical repre-sentation of propositional knowledge bases. In

ICJAI, pp. 819–826, 2011.

[5] Samuel Eilenberg and Saunders Mac Lane. Nat-ural isomorphisms in group theory. In Proc. Nat.

Acad. Sci. U.S.A., Vol. 28, pp. 537–543, 1942.

[6] Samuel Eilenberg and Saunders Mac Lane. Gen-eral theory of natural equivalences. Trans. AMS, Vol. 58, No. 2, pp. 231–294, 1945.

[7] Saunders Mac Lane and Ieke Moerdijk. Sheaves

in Geometry and Logic. Springer, 1992.

[8] C. Y. Lee. Representation of switching circuits by binary-decision programs. The Bell System

Technical Journal, Vol. 38, No. 4, pp. 985–999,

1959.

[9] Shin-ichi Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In

DAC, pp. 272–277. ACM, 1993.

[10] Masaaki Nishino, Norihito Yasuda, Shin-ichi Mi-nato, and Masaaki Nagata. Zero-suppressed sen-tential decision diagrams. In AAAI, pp. 1058– 1066, 2016.

[11] Knot Pipatsrisawat and Adnan Darwiche. New compilation languages based on structured de-composability. In AAAI, pp. 517–522, 2008. [12] 戸田貴久, 斎藤寿樹, 岩下洋哲, 川原純, 湊真一.

ZDD と列挙問題―最新の技法とプログラミング ツール. コンピュータソフトウェア, Vol. 34, No. 3, pp. 97–120, 2017.