DEIM Forum 2019 I1-4

変数シフトの導入による項分岐決定図の省空間化
Variable Shift SDD: A More Succinct and Canonical Sentential Decision Diagram
中村 健吾†

伝住

周平††

西野

正彬†

† NTT コミュニケーション科学基礎研究所 〒 619–0237 京都府相楽郡精華町光台 2-4†† 東京大学大学院情報理工学系研究科 〒 113–8656 東京都文京区本郷 7-3-1
E-mail: †{kengo.nakamura.dx,masaaki.nishino.uh}@hco.ntt.co.jp, ††denzumi@mist.i.u-tokyo.ac.jp
あらまし

論理関数や組合せ集合の圧縮索引として，二分決定図 (BDD) が広く用いられているが，近年その一般化である項分岐決定図 (SDD) が提案され，圧縮性能の良さと索引としての機能性の高さから注目を集めている．本稿では，SDD をより圧縮して保持しつつ，索引としてのクエリ処理の機能を SDD と同様に併せもつ，変数シフト

SDD(VS-SDD) というデータ構造を提案する．VS-SDD は対称性のある論理関数や組合せ集合に対して SDD と比べ圧縮性能が良くなることを理論と実験の両面で確かめた．
キーワード 決定図，論理関数，組合せ集合，集合族，変数シフト，対称性*

1 はじめに&アイテム集合が与えられたときに，そのアイテムの選び方の集合，すなわち部分集合の集合を取り扱う場面は数多い．例え'ば図 1(a) のように，論理回路は出力を true にするような入力変数の組合せを全て集めることで，論理関数としてだけでなく

%
(

!

"

#

$

































































• &, '• %, '• %, &• %, &, '+部分集合の集合としても表せる．また，図 1(b) のように，所与のグラフに対して特定の条件，例えばマッチングやパス，連結グラフなど，を満たす部分グラフを列挙する問題を考えると，各辺をアイテムだと思えば，辺の組合せのうち条件を満たすも

図 1 組合せ集合を扱う例．(a) 論理回路，(b) 部分グラフ構造列挙．

の全てをもつことになるので，やはり集合の集合を扱う．論理関数や集合の集合 (組合せ集合，集合族) の中身を仮に列挙で(3) 様々な有用なクエリや操作をサポートすること，が挙げらきれば，例えば前者の例では論理回路の設計や動作の検証なれる．表現の一意性により，各々BDD で表現された 2 つの論

ど，後者の例では配電網の損失最小化やネットワーク信頼性の理関数が等価であるかのチェックが構造の同一性のチェックで行

計算などに応用できる．しかし，論理関数や集合族を扱う際にえて，これは CUDD [26] などの BDD パッケージでは定数時間

は，しばしば組合せ爆発ともよばれる，扱う集合の数が問題サで行える．また，一度論理関数を BDD で表現すれば，出力をイズに対して指数的に増加する現象に見舞われる．例えば，図true にするような入力変数の組合せの数え上げ (モデルカウン

1(b) のようなグリッドグラフにおける対角間パスの列挙では，

ト) や，他の BDD で表現された論理関数との AND や OR な

11 × 11 グリッドでもパスの数は 1024個に達する．従って，たどの演算が，BDD の DAG 構造をほどくことなく行える．近だ列挙するだけでは表現が大きくなりすぎるので，このような

年 BDD は，ネットワークの影響拡散の厳密計算 [17] や，ネッ

論理関数や集合族をコンパクトかつ扱いやすい「索引」としてトワーク信頼性の近似計算 [25]，厳密最大化 [20] など，ネット保持するための研究が古くから行われている．

ワークにまつわる計算と最適化によく使われている．

そ の 中 で も ，二 分 決 定 図 (Binary Decision Diagram,

近 年 ，BDD の 一 般 化 と し て ，項 分 岐 決 定 図 (Sentential

BDD) [6] は特に有名で，論理関数 の表現形として広く用

Decision Diagram, SDD) [10] が提案され，注目を集めてい

1

いられている．BDD は論理関数を有向非巡回グラフ (Directed

る [14], [23]．SDD は論理関数を表現する際のサイズについて

Acyclic Graph, DAG) で表現する．BDD が広く用いられる理

BDD よりもタイトな上限をもち [10]，さらに SDD が BDD よ由として，(1) 応用上現れる様々な論理関数や集合族が理論的・

りも指数倍小さくなるような論理関数も存在することが知られ経験的に小さく表現できること，(2) 一定の条件下で，同じ論ている [4]．また，SDD は BDD と同様に一定の条件下で表現

理関数を表現すると全く同じ BDD になること (表現の一意性)，の一意性を有し，さらに文献 [11] にあるような標準的なクエリや操作をサポートする．従って，SDD は BDD より小さな表現

1：図 1(a) のように，論理関数から等価な集合族に変換できて，逆もまた然りなので，以後は特に断りのない限り「論理関数」と「集合族」を同一視する．

を実現し，かつ索引としての機能性を BDD と同様に備える．

本稿では，SDD をより小さく圧縮して表現する，変数シフ(a)ト SDD(Variable Shift SDD, VS-SDD) というデータ構造を

(b)

3

3
>

C

5

1

¬B

提案する．VS-SDD は BDD や SDD と同様に一定の条件下で
0 2
4 6
B A D C

表現の一意性をもち，また文献 [11] に挙げられたクエリや操

1B ¬A ¬B ⊥ B A ¬B ⊥ D C ¬D ⊥作のうち SDD がサポートするものは同様にサポートする．ま(c)た，VS-SDD は同じ論理関数を表す SDD より大きくなることはない．さらに，VS-SDD で表現する方が SDD で表現するよ

(d)

4
0
A

りもサイズが指数倍小さくなるような論理関数が存在するこ

4
¬A

A

5

5

1
B

とも示した．すなわち，VS-SDD は SDD より小さな表現を実

6

B > ¬B

3
2
C D

現し，なおかつ索引としての機能性を SDD と同様に備える．

6
C D ¬C ⊥VS-SDD は，対称性を備える論理関数や集合族を特に小さく表現することができ，いくつかの対称性があるベンチマーク論理

51

図 2 (a) vtree の例．(b) 関数 f = (A ∧ B) ∨ (B ∧ C) ∨ (C ∧ D) を表す，(a) の vtree に従う SDD の例．(c) vtree の例．(d) 関数

関数を，SDD よりも小さく表現できることを実験的に示した．

f = (A ∧ B) ∨ (C ∧ D) を表す，(c) の vtree に従う SDD の例．

類似研究として，より一般的な決定図である FBDD や DDG
を論理関数の対称性を取り入れて小さく表現する Sym-FBDDと Sym-DDG [2] がある．これらは変数の置換も扱えるため，
変数シフト SDD よりも多くの対称性を扱える．しかし，Sym-

FBDD/DDG のもととなる FBDD/DDG には SDD には不可
欠な vtree のような構造が無いので，このアイデアを SDD へと直接導入することはできない．また，Sym-FBDD/DDG は

conditioning や Apply といったいくつかの重要なクエリや操作をサポートしない．

たちを Y とする X-分割を表現している．vtree の例を図 2(a)に示す．この vtree は，まず 4 つの変数 {A, B, C, D} に対し{A, B}-分割を適用し，次いで左側の {A, B} にさらに {B}-分
割を，右側の {C, D} にさらに {D}-分割を適用することを表す．vtree の各ノードには，図 2(a) のように番号をつけておく．

vtree を用いると，SDD とそれが表す論理関数は次のように再帰的に定義できる．ここで，SDD α に対し，α が表す論理関数を ⟨α⟩ と表す．

2 項分岐決定図 (SDD)
まず，SDD [10] の構造について導入する．SDD は BDD と

定義 1 vtree v に従う SDD は，次のいずれかである．

•⊤ や ⊥ は，それ自体が SDD である．ここで，⟨⊤⟩ = true，

同様に，論理関数を DAG として表現するデータ構造である．

すなわち恒真関数，⟨⊥⟩ = false，すなわち恒偽関数である．こここで以後の説明のため，表記のルールを導入する．まず，大れらの SDD を定数とよぶ．

文字アルファベットで 1 つの変数，小文字アルファベットでそ•

変数 X に対し，v が変数 X に対応する葉を含むならば，の中身の値 (true もしくは false) を表す．また，太字の大文字X や ¬X は v に従う SDD である．⟨X⟩ = X ，⟨¬X⟩ = ¬X でアルファベットで複数変数の集合，小文字アルファベットでそある．これらの SDD をリテラルとよぶ．

の中身の値たち (インスタンス化) を表す．

•

p1 , . . . , pn は v の 左 の 子 ノ ー ド 以 下 に 従 う SDD で ，

論理関数 f が引数にとる変数たちを Z，その分割を X, Y と⟨p1 ⟩, . . . , ⟨pn ⟩ は互いに素，s1 , . . . , sn は v の右の子ノード以する．すると，f は X の変数のみからなる論理関数 p1 , . . . , pn下に従う SDD とする．このとき，これらを各々ペアにしたと ，Y の 変 数 の み か ら な る 論 理 関 数 s1 , . . . , sn を 用 い て ，∨f (Z) = ni=1 [pi (X)∧si (Y)] と分解できる．これを f の (X, Y)-{(p1 , s1 ), . . . , (pn , sn )} は v に従う SDD である．この SDD は[⟨p1 ⟩ ∧ ⟨s1 ⟩] ∨ · · · ∨ [⟨pn ⟩ ∧ ⟨sn ⟩] という論理関数を表す．この分解とよぶ．このとき，n をこの分解のサイズとよぶ．特に，ような SDD を分解ノードとよぶ．

(X, Y)-分解であって，任意の i =| j に対し pi ∧ pj = false か
∨
p
=
true
かつ，任意のi に対し pi =| false (互い
つ， n
i=1 i

SDD α のサイズは，α 中で用いられる全ての分割のサイズのに素) であるものを，X-分割とよぶ．以降，本稿では X-分割

図 2(b) は，関数 f = (A ∧ B) ∨ (B ∧ C) ∨ (C ∧ D) を表す，

和として定義し，|α| で表す．

を f = {(p1 , s1 ), . . . , (pn , sn )} のように表現する．このとき，

図 2(a) の vtree に従うサイズ 9 の SDD を表す．図中で，丸い

p1 , . . . , pn (左側) をプライム，s1 , . . . , sn (右側) をサブとよぶ．

ノードはそれぞれ分解ノードを表し，中に書いてある数字は，

もし X-分割が任意の i =| j に対し si =| sj を満たすならば，こそのノードがどの vtree ノードに従っているかを番号で表しての分割は compressed である，という．

いる．例えば，図 2(b) の SDD の一番上のノードでは，f は

SDD は論理関数を，X-分割を繰り返し適用して分解してゆくことにより表現するデータ構造である．このとき，どのよう((¬A ∧ B) ∧ C) ∨ (A ∧ B) ∨ (¬B ∧ (C ∧ D)) と分解されている．
SDD は次のような操作ができる．論理関数 f に対して，fに変数を (X と Y に) 再帰的に分割してゆくかを決めるのが，を true にするような，変数への true と false の割り当て方のvtree とよばれる二分木である．vtree の葉のそれぞれは論理関

総数を f のモデルカウントとよぶ．SDD α に対し，α が表す数に用いられる変数と 1 対 1 対応している．各内部ノードは，論理関数のモデルカウントを計算するのは O(|α|) 時間ででき

左側の部分木にある変数たちを X，右側の部分木にある変数

る．モデルカウントの応用については後述する．次に，論理関数 f と g を論理和 ∨ や論理積 ∧ などの演算で組み合わせるこに，正式に定義する．例えば，図 2(b) の SDD では，下側中央と (Apply 演算) も，SDD のままで可能である．より具体的にの番号 1 がついたノードは A ∧ B という論理関数を，下側右は，関数 f を表す SDD α と関数 g を表す SDD β が与えられの番号 5 がついたノードは C ∧ D という論理関数を表す．まれば，α と β が同じ vtree に従う限り，f ∨ g や f ∧ g などのた，図 2(a) の vtree で，1 番の部分木と 5 番の部分木は変数関数を表す SDD を O(|α||β|) 時間で作れる．この操作は論理以外は全く同じ構造をしており，B を D，A を C に置き換え関数から SDD を作る際に直接使えるほか，集積回路などのシることによって互いに行き来できる．ここで，同様の変数の置

ステムの論理設計や検証でも頻繁に用いられる．

き換えを A ∧ B という論理関数に対して行うと，C ∧ D とな

また，SDD は次のような制限を加えることで表現の一意性

る．さらに，図 2(b) の SDD で下側中央のノード以下の構造にを保証できる．ある SDD のクラス (集合) がカノニカルである

同様の変数の置き換えを行うと，下側右のノード以下の構造そとは，vtree が所与であるときに，任意の論理関数 f に対して，のものが得られる．このような分解ノードの組を一つにまとめf を表す SDD がそのクラス中に唯一つ存在するということでることを目指す．ここで正式な定義のためにいくつかの記号をある．SDD では 2 つのカノニカルなクラスを考えられる．

導入する．SDD α とその分解ノード q に対し，α(q) で α の q

定義 2 SDD α は，α 中で用いられる全ての分割が compressedであるとき，compressed であるという．α は，{(⊤, β)} や{(β, ⊤), (¬β, ⊥)} の形の分割をもたないとき，trimmed であるといい，一方で {(⊤, ⊤)} や {(⊤, ⊥)} の形の分割をもたないときは lightly trimmed であるという．α は，全ての分割において，p1 , . . . , pn が左の vtree 子ノード，s1 , . . . , sn が右の vtree
子ノードにちょうど従うとき，normalized であるという．

以下の部分構造 (SDD) を表す．また，vtree v のノード v1 , v2に対し，v1 ∼ v2 で，各々を根とする部分木が葉に付随する変数以外構造が同一であるということを表す．このとき，hv1 ,v2を，v1 の変数から v2 の変数への写像であって，v1 の葉の各変
数 X を hv1 ,v2 (X) に置換することで v2 が得られるようなものとする．なお，∼ は vtree ノード間の同値関係になる．
定義 4 vtree v に従う SDD α について，α 中の 2 つの分解ノー
ド q, r は次の条件を満たすとき合同であるという．(1) vq を q定理 3 ( [10]) Compressed かつ trimmed な SDD はカノニカルである．また，compressed かつ lightly trimmed かつ normal-

ized な SDD もカノニカルである．
なお，SDD α が与えられたときに α を trimmed にするのが従う vtree，vr を r が従う vtree とすると vq ∼ vr ．(2) α(r)は α(q) 中の各リテラル X, ¬X を hvq ,vr (X), ¬hvq ,vr (X) で置
き換え，各分解ノードが従う vtree ノード番号も書き換えることにより得られる．

は，{(⊤, β)} や {(β, ⊤), (¬β, ⊥)} の形の分割を β に置き換え

定 義 5 vtree v が 与 え ら れ た と き ，使 う 変 数 が そ れ ぞ れる操作をボトムアップに行えばできる．同様にして α を lightly

B(f ), B(g) である 2 つの論理関数 f, g は次の条件を満たす

trimmed や normalized にすることもできる．

とき v の下で同型であるという．(1) vf を，葉の変数が B(f )SDD が小さな表現を実現する理由の一つに，もし分解の途と一致する v の部分木とする．同様に vg を定める．すると

中で全く同じ論理関数が部分関数 (プライムやサブ) として複数

vf ∼ vg ．(2) g は f 中の各変数 X を hvf ,vg (X) に置き換える出てきたとしても，その論理関数を表す SDD は一つだけ作れことにより得られる．

ばよい，という点が挙げられる．これを部分構造の共有とよぶ．
図 2(d) の SDD では，番号 4 がついた分解ノードは C ∧ D という論理関数を表しているが，このノードは 2 箇所から参照されている．これは，論理関数を分解する途中で C ∧ D という関数が 2 回出てきたことを意味するが，この場合でも，C ∧ D を表現する分解ノードは一つあればよい．

3 変数シフト項分岐決定図 (VS-SDD)

図 2(b) の SDD で，下側中央のノードと下側右のノードは合同であり，これらが表す論理関数 A ∧ B と C ∧ D は，図 2(a)の vtree の下で同型である．
さて，合同なノードを一つにまとめるためにはどうすればよいだろうか．もとの SDD では，各分解ノードは従う vtree ノー
ド番号を明示的にもち，各リテラルはそのまま保持される．しかし，合同な分解ノードは異なる vtree ノードに従い，それ以下の部分構造中のリテラルも異なるので，もし合同な分解ノー

ここから，本稿で提案する変数シフト項分岐決定図 (VS-SDD)

ドを一つにまとめるのであれば，これらの情報は明示的に保持について説明する．VS-SDD のアイデアは，SDD のように全してはならない．そこで，VS-SDD では (i) vtree ノード番号

く同じ論理関数が出てきた場合に部分構造の共有を起こすだけのつけ直しと (ii) 従う vtree ノード番号の差分管理という 2 段

でなく，ある特定の種類の変数の置き換えによって同じ論理関階の方法でこれを解決し，合同なノードを一つにまとめる．

数を表現するようになる場合にも部分構造の共有を起こすよう

まず (i) について考える．もとの SDD では，vtree ノード番にすることである．もしこれが可能ならば，従来の SDD と比号は任意につけてよいものなので，番号づけをするルールを固べて部分構造の共有を起こせる場所が増えるため，SDD より定してしまっても SDD の応用範囲が制限されることはない．

小さな論理関数の表現を得られる．これを達成するために，従そこで，ここでは vtree のノードを一定の規則で辿って，そのう vtree ノード番号 (図 2(b) や (d) でいうと丸ノードの中に書辿った順番に従い 1 から順番に番号をつけることを考える．こかれた数字) を差分的に管理する方法を提案する．

こで「一定の規則」とは，次の 3 つの操作を各ノードで決めら

まず，「特定の種類の変数の置き換え」を例を用いて述べた後れた順番で行うことをいう．

(a)ば，図 3(b) において，下側中央と下側右の分解ノードは元々合

1

1
1

3 4
6 7
B A D C

6

>
1

2 1

なっている．こうして生ずる同一な部分構造を共有することに2

よって，ノード数の削減を達成できる．図 3(b) で生じた同一B A D C(c)

1
1

同であったが，変換後にはそれ以下の構造も含めて全く同一に

5

2

(b)

4

¬2

1
6

4

1

>
1

な部分構造を共有することにより得られる構造を図 3(c) に示¬2
4

す．このように，vtree ノード番号の差を考える変換を行って，それにより生じた同一な部分構造を共有することによって得られる構造を VS-SDD とよぶ．なお，「変数シフト」の呼び名は，

1 ¬2 ¬1 ⊥ 1 2 ¬1 ⊥ 1 2 ¬1 ⊥1 ¬2 ¬1 ⊥ 1 2 ¬1 ⊥

文献 [19] の variable shifter を元にしている．Variable shifter

図 3 (a) 図 2(a) の vtree の行きがけ順番号づけと，その差分番号づは複数の BDD をまとめて表現する際のサイズを小さくするたけ．(b) 図 2(b) の SDD で，vtree ノード番号を差分的に考えめに考案されたものである．しかし，variable shifter は変数のた構造．(c) (b) で同一な部分構造を共有したもの．

順番 (番号) に注目するものだが，本稿での変数シフトはより一
般に vtree ノード番号に注目している．

•(L) 左の子ノードの部分木を再帰的に辿る．

VS-SDD を構築するには，もとの SDD から変換する方法•(R) 右の子ノードの部分木を再帰的に辿る．

と，表したい論理関数から直接構築する方法がある．ここでは•(N) 自分自身のノードを辿る．

前者について説明する．もとの SDD α を VS-SDD へと変換

特に，各ノードで (N)→(L)→(R) という順番で操作を行って得するアルゴリズムを Algorithm 1 に示す．ここで，SDD α にられる順番を行きがけ順とよぶ．例として，図 2(a) の vtree の対して，α が従う vtree ノードを v(α) と表し，vtree ノード

行きがけ順による番号づけを図 3(a) に示す．以降の説明は行v に対してその行きがけ順による番号を num(v) とする．また，

きがけ順を用いて行うが，行きがけ順以外でも「一定の規則」

vtree ノード w に対し，e(w) を，v のノードで部分木の構造がの下で順番づけする限りはどの方法でもよい．この番号づけのw の部分木と一致するもののうちノード番号が最も小さいもの

ポイントは以下の補題にまとめられる．

の番号とする．変数の個数を m とすれば，全ての e(·) の値を

補題 6 T を n ノードの根付き順序木として，T のノードの「一定の規則」による 1 から n までの番号づけを考える．もし，Tの v を根とする部分木と w を根とする部分木がノード番号以
外順序木として同一ならば，これらの差分番号づけも同一になる．ここで差分番号づけとは，木の各辺でその両端のノード番号の差をもたせたものである．

O(m) 時間で求められるので，この値は前もって計算しておく．
Algorithm 1 の中で，リテラルを変換する処理は 7,8 行目，分解ノードを変換する処理は 9 行目にある．アルゴリズムの内部
では ConvTable と UniqTable という 2 つの連想配列を用いる．

ConvTable は，入力の SDD α のノードと，出力の VS-SDD のノードとの対応関係を保持する．UniqTable は，もしすでに合同な部分構造が処理されていたらその処理結果の VS-SDD を同一な構造の部分木は一定の規則の下では同じように辿られ返すような連想配列である．ここで e が，従う vtree ノードのるので，この補題が成立する．例えば，図 2(a) の右側は，行き部分木の構造が同一であるか判定するために用いられている．

がけ順のノード番号に対して差分番号づけを描いたものである

もしまだ合同な部分構造が処理されていなければ (12 行目)，13

が，行きがけ順番号 2 の部分木と 5 の部分木では，その差分番行目で CreateNewNode で新たな分解ノードの VS-SDD を作る．

号づけは全く同じになる．

SDD α に対し，VS(α) を α の変数シフト形とよぶことにする．

続いて (ii) について考える．まず，各分解ノードで従う vtree
ノード番号を明示的に保持する代わりに，分解ノードを指す各辺に，指す先の分解ノードが従う vtree ノード番号と，指す元

命題 8 SDD α が与えられると，その変数シフト形は O(|α|) 時間で計算できる．

のノードが従う vtree ノード番号の差をもたせる．次に，各リ

最後に VS-SDD の基本的な性質をいくつか示す．まず一つテラルをそのまま保持する代わりに，そのリテラルの変数に対は表現の一意性である．実は，Algorithm 1 の VS は SDD と応する葉の vtree ノードの番号と，そのリテラルを分解の一部

VS-SDD の間の全単射の写像であることが示せるので，SDDとしてもつ分解ノードが従う vtree ノード番号の差をもたせる．

と VS-SDD の間には一対一関係がある．従って，VS-SDD に対

ここで使用する vtree ノード番号は，行きがけ順番号づけによしても，compressed, trimmed, lightly trimmed, normalized

るものである．図 2(b) の SDD に，図 3(a) にある vtree の行の 4 つの性質を，対応する SDD がその性質をもつかどうかできがけ順番号づけを考えた上で，vtree 番号の差分化を行なっ定義できる．すると，カノニカルな SDD のクラスからカノニた構造を図 3(b) に示す．すると，次の補題が成立する．

カルな VS-SDD のクラスを導ける．

補題 7 vtree ノードが一定の規則により番号づけされているな

定理 9 Compressed かつ trimmed な VS-SDD はカノニカルでらば，上記の操作により，合同なノードは全く同一な部分構造ある．また，compressed かつ lightly trimmed かつ normalizedに変換される．

な VS-SDD もカノニカルである．

この補題は合同性の定義 (定義 4) と補題 6 より示せる．例え

次に VS-SDD のサイズについて，Algorithm 1 の VS では，

Algorithm 1 SDD α を VS-SDD に変換する手続き VS(α)．
入力： 分解ノードの SDD α.
出力： α を VS-SDD へと変換した構造.
1: if ConvTable(α) =| nil then2:
return ConvTable(α)
3: else4:γ ← {}
5:for all α 中の要素 (pi , si ) do
6:
if pi が定数 then p ← pi
7:else if pi がリテラル then p ← num(v(pi )) − num(v(α))
8:else if pi が 否 定 リ テ ラ ル then p ← ¬(num(v(pi )) −num(v(α)))
9:else p ← (num(v(pi )) − num(v(α)), VS(pi ))10:(s と si に対しても同様の処理を行う)
11:
要素 (p, s) を γ に加える
12:
if UniqTable(e(v(α)), γ) = nil then
13:
UniqTable(e(v(α)), γ) ← CreateNewNode(γ)
14:return ConvTable(α) ← UniqTable(e(v(α)), γ)

(a)
X3

X1

X2

X4

X5

(b) v1 (X) =X6

X1

vk (X) =

X2
X1

X7

X9

X8

X11

X10

X13

X12

X2

X14
vk−1 (Y)vk−1 (Z)

図 4 (a) 各辺に変数が付随した深さ 3 の完全二分木．(b) 証明に用いる vtree vk (X) の再帰的構造．

作った vtree に対して，その compressed SDD を考えると，その中に指数的に多くの合同な分解ノードのペアが存在することがわかる．VS-SDD にすることでそれらのノードをまとめられるので，全体としてサイズ O(k) を達成できる．

4 データ構造もとの SDD で合同なノードをまとめるだけで，サイズが増加することは無いので，|VS(α)| <= |α| が成立する．
命題 10 任意の SDD α に対して，|VS(α)| <= |α|．

VS-SDD が空間効率の面でも良くなるためには，理論的性質
のみならず実装にも言及しなければならない．なぜなら，理論的な VS-SDD サイズが SDD サイズよりも小さくなったとしても，vtree ノード番号を各分解ノードではなく各辺に差分的に

3. 1 指 数 圧 縮もつことでメモリ使用量がむしろ増加してしまう可能性がある

次に注目するのは，変数シフト形に変換することでサイズがどの程度圧縮できるのか，ということである．変数の個数を mとすると，vtree の中で同じ形の部分木は最大でも m 個なので，サイズの比 |VS(α)|/|α| の下限は 1/m，すなわち最大でも m 倍の圧縮が限界である．一方で，この圧縮率を漸近的にほぼ達成する論理関数を実際に構成できる．
定理 11 論理関数の列 f1 , f2 , . . . であって，fk は O(2k ) 変数の論理関数で，fk を表す compressed SDD のサイズは任意のkvtree に対して Ω(2 ) であるが，fk を表す compressed VS-SDDのサイズはある vtree に対して O(k) になるものが存在する．

からである．残念ながら，VS-SDD がその通り実装される限り
は，VS-SDD の方がメモリ使用量が大きくなる例は存在する．
しかし，多少の変更でこの問題は回避できる．まず，normal-

ized VS-SDD に対しては，辺に付随させる vtree ノード番号の差を無視すればよい．Normalized ならばプライムが左の子ノード，サブが右の子ノードにちょうど従うので，上から辿るだけで従う vtree ノード番号を復元できるためである．一方で，一般の VS-SDD に対してはもとの SDD の再利用が考えられる．
変数シフト形に変換する際に行うのは，合同なノードを一つにまとめることである．その代わりに，例えば従う vtree ノード
番号が最も小さいものなど，合同なノードのうち代表の 1 つの本定理における圧縮率は O(k/2k ) = O(log m/m) である．定みを残すという方法も考える．このとき，他の合同なノードは

理 11 は，SDD に対してあらゆる vtree を考慮しているため，

分解 {(p1 , s1 ), . . . , (pn , sn )} をもつ代わりに，代表のノードへ

冒頭の議論よりも強い主張になっている．また，定理 11 は，のポインタを張る．分解を直接もつと，たとえ分解のサイズがVS-SDD が決定図のサイズを線形サイズから対数サイズに指数

1 でも 2 つのポインタを使うため，これを 1 つのポインタに置的に圧縮するケースがある，ということも表している．

き換えてもメモリ使用量が増加することはない．なお，このよ

詳しい過程は省略するが，定理 11 の証明では，うな構造でも VS-SDD の性質が損なわれることはない．なぜな∧2k −2 ((¬Xj ∨ ¬X2j+1 )j=1

らこの構造でも，vtree ノード番号のオフセットを保存しておfk (X) = (¬X1 ∨¬X2 ) ∧)∧ (¬Xj ∨ ¬X2j+2 ) ∧ (¬X2j+1 ∨ ¬X2j+2 ) ,という論理関数列が実際に条件を満たすことを示す．fk は，実き，上から順番にノードを辿り，合同なノード間のポインタを辿るときにノード番号の差をオフセットに足せば，従う vtree
ノード番号を復元できるからである．

は深さ k の完全二分木の部分グラフであってマッチングを成すような辺集合を考えることに相当する．図 4(a) のような完全二分木を考えると，f (x) = true となるのは，true を割り当てた変数たちに対応する辺集合がマッチングを成すとき，かつそのときに限る．定理 11 の前半は容易に示せる．一方で後半に関しては，図 4(b) にあるような vtree vk (X) に従う compressed

VS-SDD のサイズが実際に O(k) になることを示す．ここで Yは二分木で X1 以下の辺に対応する変数 (X3 , X4 , . . .)，Z は X2
以下の辺に対応する変数 (X5 , X6 , . . .) である．このようにして

5 クエリと操作
VS-SDD の重要な性質は，合同なノードを解いて SDD へと戻すことなく，SDD ができるのと同様なクエリや操作を実現できるということである．ここでは，特に文献 [11] に記された，論理関数に対する基本的なクエリや操作に焦点を当てる．これ
らのクエリや操作の基礎となるのは，Apply とよばれる操作と，(重みなし) モデルカウントである．
2 章でも述べた，論理関数のモデルカウントを求める問題は，

#SAT ともよばれ，ネットワーク信頼性の推定 [12] など幅広い

表 1 SDD (S), compressed SDD (S(C)), VS-SDD (V), compressed

分野に応用をもつ．SDD が表す論理関数のモデルカウントを

VS-SDD (V(C)) の，多項式時間で計算できる (a) クエリと (b)求めるためには，各分解ノードでそれ以下の部分構造が表す論

操作の一覧．✓ は多項式時間アルゴリズムが存在することを，•

理関数のモデルカウントの値をボトムアップに求める動的計画法を行う．ここで，同型な論理関数は同じモデルカウントをもつので，SDD 中で合同な分解ノードが表す部分論理関数もや
はり同じモデルカウントをもつ．例えば，図 2 中の合同なノードはどちらもモデルカウントが 1 である．従って，VS-SDD で同様な動的計画法を行う際に，合同なノードが何個まとめられたかに関わらずカウントの値は 1 つだけもてばよい．各カウン
ト値は動的計画法により各々の分解サイズに比例する時間で求まり，全体でも VS-SDD サイズに比例する時間で求まる．
命題 12 VS-SDD α が表す論理関数のモデルカウントの値はO(|α|) 時間で求まる．

は多項式時間アルゴリズムは存在し得ないことを示している．各
クエリや操作の説明については文献 [11] を参照．
(a) クエリS V S(C) V(C)CO
consistency
✓ ✓
✓
✓
VA
validity✓ ✓✓✓CEclausal entailment
✓ ✓
✓
✓
IM
implicant check
✓ ✓
✓
✓
EQ
equivalence check
✓ ✓
✓
✓
CT
model counting
✓ ✓
✓
✓
SE
sentential entailment ✓ ✓✓✓MEmodel enumeration ✓ ✓✓✓(b) 操作S V S(C) V(C)∧C
conjunction••••∧BC bounded conjunction ✓ ✓••∨Cdisjunction••••∨BC bounded disjunction ✓ ✓••¬Cnegation✓ ✓✓✓CD
conditioning
✓ ✓
•
•
FO
forgetting••••
SFO singleton forgetting ✓ ✓••なお，確率推論 [11], [24] などのいくつかの応用先では，各力が compressed であることを強制するためには，計算中に同変数に重みがついた重み付きモデルカウントが必要になる．

じサブが出現したら対応するプライムの OR を取って一つにま

VS-SDD α に対し重み付きモデルカウントの計算は必ずしもとめるという操作を加えればよい．しかし，SDD でこのようO(|α|) 時間ではできないが，各分解ノードに対してまとめられな操作を加えると理論上は Apply の計算が O(|α||β|) 時間で終た合同なノードの個数分だけカウンタを用意することで少なく

わらなくなってしまうことがあり [5]，VS-SDD でも同様の問とも元の SDD を用いるのと同じ時間でできる．さらに，いく

題が起こる．一方で実用上は，SDD の Apply でこのような操

つかの変数で重みが同じであれば，カウンタのうちいくつかは作を挟むことでむしろ計算が高速化したり出力サイズが小さく共有できて，SDD を用いるより計算が速くなる可能性がある．

なったりすることが多く [5]，VS-SDD でも同様である．

次に Apply とは，2 つの決定図 (この場合は VS-SDD) α, β

以上のモデルカウントと Apply に加えて，いくつかのクエと，∨ (論理和) や ∧ (論理積) のような二項演算 ◦ を受け取り，リや操作に対して固有のアルゴリズムを考えることで，表 1 の⟨α⟩ ◦ ⟨β⟩ を表す決定図を出力する操作である．この操作は，論結果が示される．ポイントは，文献 [11] に示された基本的なク理関数から直接決定図を構築するために重要であり，2 章で述

エリや操作で，SDD が多項式時間でサポートするものは全て

べた通り，SDD では O(|α||β|) 時間でこの操作を実行できる．

VS-SDD でも多項式時間でサポートする，ということである．

VS-SDD に対する Apply を考える際に重要なのは，合同性と同型性を使うことにより計算を省略できる場合がある，ということである．例えば f = A ∧ B, f ′ = C ∧ D, g = ¬A, g ′ = ¬Cに対し，f と f ′ ，g と g ′ は同型だが，このとき f ∨ g = ¬A ∨ Bと f ′ ∨ g ′ = ¬C ∨ D も同型になる．このように，用いる変数が共通する論理関数の組 (f, g), (f ′ , g ′ ) に対し，f と f ′ ，g とg ′ が同型なら，f ◦ g と f ′ ◦ g ′ や ¬f と ¬f ′ も各々同型になる．
この事実を用いると，証明は少し込み入るが，VS-SDD に対しても O(|α||β|) 時間で Apply ができることを示せる．

6 実

験

最後に，変数シフトを導入することで決定図のサイズがどれほど小さくなるかを，実験で確かめる．VS-SDD のアイデアは同型な関数を表すノードを一つにまとめることなので，ここでは対称性のある論理関数に焦点を当てる．本稿では以下の実験

A 及び B を行った．
実験 A では，CNF の形で与えられた論理関数を，動的 vtree
探索 [8] を用いて SDD へ変換し，SDD 自体のサイズとその変命題 13 同じ vtree に従う 2 つの VS-SDD α, β が与えられた

数シフト形 (VS-SDD) のサイズを比較した．CNF を SDD へとき，⟨α⟩ ∨ ⟨β⟩ や ⟨α⟩ ∧ ⟨β⟩ を表す VS-SDD を O(|α||β|) 時間と組み上げる際には，SDD package version 2.0 [9] を利用し，で構築できる．

動的 vtree 探索の際の初期 vtree は平衡二分木とする．

重要なのは，VS-SDD における Apply の計算は，SDD における Apply の計算のうち，同型性を用いることで省略できる部分を省略するような形になるので，SDD の Apply より高速にできる，ということである．命題 13 により，CNF で表された論理関数から，∨ や ∧ を順番に組み合わせることで直接

VS-SDD を構築できる．
なお，命題 13 のアルゴリズムでは，例え入力の α, β が com-pressed であったとしても，出力が compressed である，つまり各分解でサブとして同じものが出てこないとは限らない．出

ここではまず，同じく変数の置換により同じになる関数を表現するノードをまとめるというアイデアに基づいている Sym-

DDG [2] の実験でも使われた，計画問題に関する CNF のデー
タセットを用いる．決定的な計画問題は，状態変数の集合，初期状態，目標状態の集合，行動の集合の 4 つ組で表され，1 回行動を行うとそれに従って状態変数の中身が (決定的に) 変化する．期間 T が与えられたとき，この計画問題に対する計画とは，初期状態を目標状態へと変化させる，t = 0, . . . , T − 1 に対する行動の列である．計画問題を論理関数で表現する方法につい表 2 実験 A の結果．
V/S
問題及び変数個数S
V(%)
blocks-2 t3
248 8811 7057 80.1
blocks-2 t5
406 31861 28858 90.6
bomb-5-1 t3
348 3798 2278 60.0
bomb-5-1 t5
564 6327 3960 62.6
bomb-5-1 t7
780 11212 7287 65.0
bomb-5-1 t10 1104 16514 10426 63.1
comm-5-2 t3
488 20584 18033 87.6
emptyroom-4 t3 116 1822 1146 62.9
emptyroom-4 t5 188 3090 1885 61.0
emptyroom-4 t7 260 5073 3001 59.2
emptyroom-4 t10 368 106737 103417 96.8
emptyroom-8 t3 244 10511 8549 81.3
safe-5 t3
54567
441 77.8
safe-5 t5
86898
640 71.2
safe-5 t7
118 1710 1314 76.8
safe-5 t10
166 2506 1756 70.1
safe-30 t3
304 5476 4067 74.3
safe-30 t5
486 8710 6328 72.7
safe-30 t7
668 14449 10371 71.8
941 23469 17421 74.2
safe-30 t10
8-Queens
64 2222 1624 73.1
9-Queens
81 5559 4767 85.8
10-Queens100 10351 9159 88.5
11-Queens
121 30611 28876 94.3
Matching-6x6
60 13091 12671 96.8
Matching-8x8
112 98200 97103 98.8
Matching-6x18 192 36228 34241 94.5

表 3 実験 B の結果．
V/S +Implicit Partitioning V/S問題及び変数個数
B
S
V
(%)
B
S
V
(%)
8-Queens
64
4898
2647
979 37.0
2540
712
251 35.3
9-Queens
81
19110
5787
2591 44.8
9906
1538
692 45.0
10-Queens
100
51886
12260
5884 48.0 26666
3918
1984 50.6
11-Queens
121 189640
35703 23682 66.3 97489 13076
8636 66.0
12-Queens
144 870336 110407 67469 61.1 449026 37480 24837 66.3
13-Queens
169 4088784 425125 288914 68.0 2114867 159184 112703 70.8
14-Queens
196 19144832 2179800 1525922 70.0 9914781 1049888 761602 72.5
Matching-6x6
60
3692
4914
3986 81.1
2561
2587
1978 76.5
Matching-8x8
112
22832
29842 24082 80.7 15781 15691 11850 75.5
Matching-10x10
180 123956 160274 129042 80.5 85545 84235 63242 75.1
Matching-6x18
192
20588
30289 21007 69.4 14273 14346
7960 55.5
Matching-8x24
352 145712 214289 147471 68.8 100773 100874 54856 54.4
Matching-10x30
560 902196 1328145 909327 68.5 623145 622602 334088 53.7
Path-6x6
60
6980
10685
7273 68.1
4573
4751
2556 53.8
Path-8x811291438 165977 123319 74.3 60840 70254 42132 60.0
Path-10x10
180 1073156 2386085 1897815 79.5 719989 995343 670069 67.3
Path-6x18
192
29924
54911 40029 72.9 19885 21622 11772 54.4
Path-8x24
352 374830 822133 637779 77.6 251368 321357 191971 61.6
Path-10x30
560 4249716 11359107 9282557 81.7 2865909 4541423 3143189 69.2
Cardinality-10 2046
44792
77410
2064 2.7 42756 33396
1263 3.885092 131370
5360 4.1 83066 57309
3469 6.1
Cardinality-20 2046
Cardinality-50 2046 203592 272548 21090 7.7 201596 122196 14439 11.8
Cardinality-100 2046 393092 476762 60984 12.8 391146 222529 43281 19.4
Knapsack-(300,10) 300
31912
14214
7257 51.1 30613
7977
5111 64.1
Knapsack-(300,20) 300 104120
35545 29523 83.1 100938 27870 25365 91.0
Knapsack-(600,10) 600
64414
28065 11021 39.3 61849 14026
7123 50.8
Knapsack-(600,20) 600 206472
51916 36826 70.9 199891 36346 30152 83.0ては，文献 [2] を参照のこと．本実験では，Sym-DDG の実験

実験 B では，明らかな対称性がある論理関数に注目し，各でも用いられた，“blocks-2”, “bomb-5-1”, “emptyroom-4/8”,

論理関数をトップダウンコンパイラ [22] を用いて SDD に組み“safe-5/30” の各計画問題を使用する．

上げ，その変数シフト形とサイズを比較した．ここで，vtree

もう一つは，より明らかな対称性がある論理関数のデータとしては，その論理関数の対称性を取り入れたものを使用す

セットを用いる．そのうちの一つが N -クイーン問題である．こる．詳細は省くが，これらの vtree は，例えばグリッドの線対

れは，N × N のチェスボードに、N 個のクイーンを互いに干称性など明らかな対称性しか使わずに簡単に作れるものであ

渉しないよう配置する問題である．この問題に対し，ボードのる．また，ここで用いる論理関数は BDD の文献でよく現れる

各マスに変数を割り当て，true のマスにクイーンを置くと N -ものなので，良い変数順を用いた BDD ともサイズを比較した．

クイーン問題の解となるときに true となる論理関数を考える．

ここで BDD サイズは SDD のように，節点数ではなく辺の数

この論理関数は，ZDD などの決定図のベンチマークとして用で評価した．さらに，トップダウンコンパイラ [22] は，通常いられる [7], [18]．もう一つは図 1(b) のようなグリッドグラフ

Implicit Partitioning (IP) [21] というサイズ削減のテクニックの部分グラフ索引化である．文献 [15], [22] にあるように，グラを適用した SDD を出力するので，本実験では IP を適用した

フに対してある条件を満たす部分グラフを索引化することには

BDD, SDD, VS-SDD サイズも測定した．

多くの応用がある．ここで，グリッドグラフは，その構造の単使うデータセットは，実験 A でも用いた N -クイーンとマッチ

純さと比べ部分グラフの索引化が難しいため，ベンチマークとングに加え，次の 3 種類である．まず “Path-mxn” は，m × n

してよく用いられる [13]．ここでは特にマッチングを成す部分

グリッドグラフの対角コーナー間の単純パスを索引化する問題

グラフの索引化を考える．ここで，チェスボードにもグリッド
表 2 が実験 A の結果である．“S” の列は SDD サイズ，“V”

である．他の 2 種類のデータセットは，各変数を {0, 1}-変数と∑<i wi Xi = θ, wi , θ ∈ R+ を満たす組合せを索引化する問題である．ここで各 wi は重み，θ

の列は VS-SDD サイズ，“V/S” の列は SDD サイズと比べたは閾値とよばれる．このような索引化は組合せ最適化問題を解VS-SDD サイズの比を表す．ここで，計画問題の末尾の “ tn”

くのに実用的に重要である [3]．ここで，もし重みとして現れる

は，期間が T = n であることを表し，マッチング問題の末尾値の種類が少なければ，SDD を作る際に多くの同型な制約，すはグリッドサイズを表す．まず，多くの計画問題のデータに対

なわち変数は異なるが重みや閾値は同じ制約が現れることが期

し，変数シフト形のサイズは元の SDD のサイズの 60〜80%程待される．“Cardinality-θ” は，変数の個数が 2046，閾値が θ

度に圧縮できていることがわかる．V/S の列に示した圧縮率

で，全ての重みが 1 であるナップサック制約の索引化問題であは，DDG のサイズと比べた Sym-DDG [2] の圧縮率と比べて，る．“Knapsack-(m, k)” は，m 変数で，重みの値が k 種類で，同等か，一部のデータでは勝っている．一方で，N -クイーンの閾値が 300 であるナップサック制約の索引化問題である．ここデータでは N = 11 を除き相変わらず良い圧縮率が得られてい37iで，各重みは {8 + ⌊ k−1⌋ | i = 0, . . . , k − 1}，つまり区間 [8, 45]

るが，マッチングのデータでは変数シフトの効果は薄かった．

から等間隔にとった k 個の整数から一様ランダムに選んだ．

グラフにも，線対称性や点対称性があることが観察できる．

みなしたときのナップサック制約

動的 vtree 探索では，強い依存関係をもつ変数を近くに集める

表 3 が実験 B の結果である．“B” の列は BDD サイズを表す．

ことで小さな SDD を達成する傾向がある．計画問題のデータ

まず N -クイーン問題では，VS-SDD サイズは BDD や SDD のでは，近い t に関係した変数が近くに集まったことで，対称性

サイズより非常に小さく，圧縮率は全ての N で 73%以下になっをうまく捉えられたと思われる．

ている．これは VS-SDD が問題の対称性をうまく捉えられていることを表す．さらに，実験 B における SDD や VS-SDD サ
イズは実験 A よりも小さくなっている．一方で，N が大きくなると圧縮率が少し悪くなる．これは，プライム側は互いに素でなければならないが，サブ側はそうではない，という非対称性に起因すると思われる．次にナップサック制約についても，よく対称性が捉えられていることが観察できる．特に，変数の数が多く，重みの種類数が少ないほどよく圧縮が効くことがわかる．次にマッチングの問題については，IP を適用すると BDDと SDD のサイズはほぼ同程度だが，VS-SDD サイズはそれの50〜75%程度になることがわかる．最後にパスの問題について
は，SDD サイズが BDD サイズより大きくなっており，これは SDD で用いた vtree が最適ではないことを示している．それでも，IP を適用すると VS-SDD サイズは BDD サイズより小さくなっており，SDD にとっては最適ではない vtree を使っても VS-SDD では小さな表現が得られる可能性があることを示唆している．

7 関連研究と結論
ここで関連研究について述べる．BDD に対しては，追加のデータ構造を用いてより小さく表現する研究は数多くあり，その中で最も有名なのは否定枝および，variable shifter を含
む attributed edges [16], [19] である．最近は，データ構造の付加により BDD と ZDD の良いとこ取りを目指す研究もあり，

chain-reduced ZDD/BDD [7] や tagged BDD [27] が提案されている．VS-SDD によく似た構造として，変数の番号をずらす
手法を提案した ↑ ∆BDD [1] がある．このアイデアは本稿の変数シフトに似ているが，そのまま SDD の vtree に適用すると
上手くいかないので，VS-SDD では行きがけ順の変数順序を導入している．また，合同性の定義を行うことで，↑ ∆BDD ではできない O(|α||β|) 時間での Apply を可能にした．
本稿では，変数シフト SDD という，SDD をより小さく表現
するデータ構造を提案した．VS-SDD は，表現の一意性や，ク
エリや操作のサポートといった SDD の重要な性質を受け継ぐ．
また，VS-SDD のサイズは SDD より大きくなることはなく，サイズが指数倍小さくなる例も存在する．さらに，実験にて，いくつかの論理関数に対し，VS-SDD は関数の対称性を捉えてサイズが小さくなることを確かめた．

文

献[1] Anuchit Anuchitanukul, Zohar Manna, and Tomás E. Uribe.
Diﬀerential BDDs. In Computer Science Today, pp. 218–
233, 1995.
[2] Anicet Bart, Frédéric Koriche, Jean-Marie Lagniez, and
Pierre Marquis. Symmetry-driven decision diagrams forknowledge compilation. In ECAI, pp. 51–56, 2014.
[3] David Bergman, Andre A. Cire, Willem-Jan van Hoeve,
and John Hooker. Decision Diagrams for Optimization.
Springer International Publishing, 2016.
[4] Simone Bova. SDDs are exponentially more succinct than
OBDDs. In AAAI, pp. 929–935, 2016.
[5] Guy Van den Broeck and Adnan Darwiche. On the role ofcanonicity in knowledge compilation. In AAAI, pp. 1641–

1648, 2015.
[6] Randal E. Bryant. Graph-based algorithms for booleanfunction manipulation. IEEE Trans. Comput., Vol. C-35,
pp. 677–691, 1986.
[7] Randal E. Bryant. Chain reduction for binary and zerosuppressed decision diagrams. In TACAS, pp. 81–98, 2018.
[8] Arthur Choi and Adnan Darwiche. Dynamic minimizationof sentential decision diagrams. In AAAI, pp. 187–194, 2013.
[9] Arthur Choi and Adnan Darwiche. The SDD package: version 2.0. http://reasoning.cs.ucla.edu/sdd/, 2018.
[10] Adnan Darwiche. SDD: a new canonical representation of
propositional knowledge bases. In AAAI, pp. 819–826, 2011.
[11] Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., Vol. 17, pp. 229–264,
2002.
[12] Leonardo Duenas-Osorio, Kuldeep S. Meel, Roger Paredes,
and Moshe Y. Vardi. Counting-based reliability estimation
for power-transmission. In AAAI, pp. 4488–4494, 2017.
[13] Hiroaki Iwashita, Yoshio Nakazawa, Jun Kawahara, Takeaki
Uno, and Shin-ichi Minato. Eﬃcient computation of thenumber of paths in a grid graph with minimal perfect hashfunctions. Technical Report TCS-TR-A-13-64, Division ofComputer Science, Hokkaido University, 2013.
[14] Doga Kisa, Guy Van den Broeck, Arthur Choi, and Adnan
Darwiche. Probabilistic sentential decision diagrams. In
AAAI, pp. 558–567, 2014.
[15] Donald E. Knuth. The Art of Computer Programming,Vol. 4A: Combinatorial Algorithms, Part I. Addison-Wesley,
2011.
[16] Jean-Christophe Madre and Jean-Paul Billon. Proving circuit correctness using formal comparison between expected
and extracted behaviour. In DAC, pp. 205–210, 1988.
[17] Takanori Maehara, Hirofumi Suzuki, and Masakazu Ishihata. Exact computation of influence spread by binary decision diagrams. In WWW, pp. 947–956, 2017.
[18] Shin-ichi Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In DAC, pp. 272–277, 1993.
[19] Shin-ichi Minato, Nagisa Ishiura, and Shuzo Yajima. Sharedbinary decision diagram with attributed edges for eﬃcientboolean function manipulation. In DAC, pp. 52–57, 1990.
[20] Masaaki Nishino, Takeru Inoue, Norihito Yasuda, Shin-ichi
Minato, and Masaaki Nagata. Optimizing network reliability via best-first search over decision diagrams. In IEEE
INFOCOM, pp. 1817–1825, 2018.
[21] Masaaki Nishino, Norihito Yasuda, Shin-ichi Minato, andMasaaki Nagata. Zero-suppressed sentential decision diagrams. In AAAI, pp. 1058–1066, 2016.
[22] Masaaki Nishino, Norihito Yasuda, Shin-ichi Minato, andMasaaki Nagata. Compiling graph substructures into sentential decision diagrams. In AAAI, pp. 1213–1221, 2017.
[23] Umut Oztok and Adnan Darwiche. A top-down compiler
for sentential decision diagrams. In IJCAI, pp. 3141–3148,
2015.
[24] Tian Sang, Paul Beame, and Henry Kautz. Performing
Bayesian inference by weighted model counting. In AAAI,
pp. 475–481, 2005.
[25] Yuya Sasaki, Yasuhiro Fujiwara, and Makoto Onizuka. Efficient network reliability computation in uncertain graphs.
In EDBT, 2019. to appear.
[26] Fabio Somenzi. Eﬃcient manipulation of decision diagrams.
Int. J. Softw. Tools Technol. Transf., Vol. 3, pp. 171–181,
2001.
[27] Tom van Dijk, Robert Wille, and Robert Meolic. Tagged
BDDs: combining reduction rules from diﬀerent decision
diagram types. In FMCAD, pp. 108–115, 2017.