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

SAT ソルバーを用いた高速な部分グラフ探索ツールの
実装と評価
川原 征大

宋 剛秀

番原 睦則

田村 直之

部分グラフ探索とは，与えられたグラフから制約を満たす部分グラフを見つけることであり，回路配線等の様々な応用が知られている．本論文では，SAT ソルバーを用いた高速な部分グラフ探索ツールを提案・評価する．既存研究としては Zero-suppressed decision diagram(ZDD) を用いた部分グラフ探索ツール Graphillion がある．ZDD は解の数が多くなっても高速に全列挙可能という特長を持つが，大きなグラフでは ZDD の構築に失敗することがある．一方，SAT ソルバーは大規模な問題に対しても，高速な単解探索が可能であるという特長を持つ．本研究ではまず部分グラフ探索で使われるグラフ上の制約の SAT 符号化方法を提案する．特に頂点の連結性に関する制約モデ
ルについては推移関係を用いた方法と次数の制約を用いた方法の 2 種類を提案する．計算機実験の結果，k クリーク問題，マルチパス問題，ハミルトン閉路の単解探索において，ZDD が利用不可能な 1000 頂点以上のグラフでも高速に求解できることを確認した．

Subgraph search is to ﬁnd subgraphs satisfying given constraints, and it has various applications such as
circuit wiring. In this paper, we propose and evaluate a subgraph search tool using SAT solvers. There is awell known subgraph search tool Graphillion using ZDD, which can enumerate over millions of subgraphs.
However, it fails to construst ZDD when a given graph becomes large. On the other hand, the advantage of
SAT solver is that it can ﬁnd one solution even if a given graph becomes large. In the proposed method, we
ﬁrst formalize constraints on graphs as CSP. In particular, for connectivity constraints, we propose transitivity constraint model and degree constraint model. Then, we ﬁnd subgraphs by using SAT-based constraint
solver. We evaluate the performance of the proposed tool on k-Clique Problem, multi-path problem and
Hamiltonian Cycle Problem, and conﬁrm it works well on graphs of over 1000 nodes which cannot be solved
by ZDD.

目は部分グラフをグラフ理論における専用アルゴリ

1 はじめにズムを用いて求めるツールであり [16] [17] [5]，二つ目部分グラフ探索とは，与えられたグラフから制約をは部分グラフが満たすべき条件を制約式で表して汎満たす部分グラフを見つける探索のことである．部分

用的なソルバーを用いて求めるツールである [8]．一グラフ探索には電子回路設計などの様々な実世界のつ目のツールは専用アルゴリズムを用いた高速な求応用があり，部分グラフ探索を高速に行うツールを研解が特長であるが，部分グラフに追加の条件があった

究・開発することは重要である [8] [16] [17] [5]．

場合にはアルゴリズムを書き換える必要があり対応

部分グラフ探索ツールは大きく 2 種類ある．一つが難しい．一方，二つ目のツールは汎用的なソルバーを使うため，専用アルゴリズムに比べて求解性能が劣SAT ソルバーを用いた高速な部分グラフ探索ツールの実
装と評価
Masahiro Kawahara, 神戸大学大学院システム情報学研
究科, Graduate School of System Informatics, Kobe
University.
Takehide Soh, Mutsunori Banbara, Naoyuki Tamura,
神戸大学情報基盤センター, Information Science andTechnology Center, Kobe University.

ることがあるが，追加の条件に対して新たに制約を記述することで対応することができる．
二つ目の汎用的なソルバーを用いる部分グラフ探索
ツールの代表的なものとして Zero-suppressed deci-sion diagram (ZDD) [13] を用いた Graphillion†1 が号化する．これらの提案方法をまとめて部分グラフ探提案・公開されている [8]．Graphillion はフロンティア

索ツール Scarabellion の実装を行った．

法を利用した ZDD 構築アルゴリズム [10] [11] によっ

提案方法を評価するために，k クリーク問題，マルて，制約を満たす部分グラフ集合を高速に全列挙可能

チパス問題，ハミルトン閉路問題を用いた計算機実験という特長を持っている．これまで電力網の評価 [9]や鉄道網分析 †2 など実問題への応用が活発に行われを行った．その結果，提案方法を実装した Scarabellion

るなど，Graphillion は優れた部分グラフ探索ツール

くの問題を高速に解き，またより大きなグラフの問題である．しかしながら，探索対象となる与えられたグを解くことができることを確認した．また提案した 2

ラフのサイズが大きくなると ZDD の構築に非常につの制約モデルについても，それぞれ異なる問題に適時間がかかったり，メモリ不足のために ZDD の構築していることを確認した．

は既存ツールである Graphillion と比較して，より多ができないことがある．この場合，部分グラフを 1 つ

本論文の構成は以下のようになる．まず 2 節で部も得られないため，ZDD の構築ができない大きなグ

分グラフ探索問題とグラフ制約を定義する．3 節でそラフに対しても高速に解を返すことができる汎用的の制約モデルを説明する．4 節では制約モデルを実装

な部分グラフ探索ツールの研究が課題となっている．

した部分グラフ探索ツール Scarabellion について説明

命題論理の充足可能性判定問題 (SAT) は与えらする．5 節では提案方法を評価するための計算機実験れた連言標準形の命題論理式を充足する値割り当てについて説明する．6 節で本論文のまとめを行う．

を見つける問題であり，SAT 問題を解くプログラム
は SAT ソルバーと呼ばれる [2] [7] [15]．近年の SAT

2 部分グラフ探索問題

ソルバーの性能向上は目覚ましく，数百万変数から

本節では，まず部分グラフ探索問題とその制約につ構成されるような巨大な SAT 問題でも高速に単解

いて説明を行い，その具体例を示す．

を計算可能である．このような SAT ソルバーの求解性能を利用した問題解法が様々な分野で成功を収

2. 1 部分グラフ探索問題と制約めており [7] [1] [23] [14], 特に整数有限領域上の制約充

V を頂点集合，E を辺集合とするとき，部分グラフ

足問題 (CSP) を SAT に符号化して SAT ソルバー

探索の入力となるグラフ（ユニバース）を G(V, E) でで解く SAT 型制約ソルバーが多く開発されている定義する．部分グラフ探索問題 とは与えられた制約を[22] [20] [24] [12] [6] [21]．

全て満たすユニバースの全域部分グラフ G(V, E) ⊂ G

本論文では，SAT ソルバーを用いた新しい部分グを求める問題である．

ラフ探索の方法を提案し，提案方法を実装したツール

部分グラフ探索で入力として与えられる制約には

Scarabellion を使ってその性能の評価を行う．SAT ソ

様々なものが考えられるが，本研究では代表的な部分

ルバーを用いて部分グラフ探索を行うために，本論文

グラフ探索ツールの一つである Graphillion [8] で用い

ではまず部分グラフ探索問題とグラフ制約の定義をられている以下 5 つの制約を対象とする．これらの行い，その制約モデルを提案する．特にグラフ制約の一つ一つは単純な制約であるが，組み合わせることで中でも頂点の連結に関する制約は SAT 符号化した際様々なグラフ上の問題を汎用的に記述することが可能の符号化節数が多くなることが問題となるが，本研究になっている．ここで括弧内は Graphillion の中で使ではこの制約に対し推移モデルと次数モデルという 2われている制約名である．

つの異なる特長を持つ制約モデルを提案する．最終的• 頂点集合制約 (Vertex Groups)に部分グラフ探索問題は提案した制約モデルと SAT

入力: 頂点集合の集合 {V1 , ..., Vm }型制約ソルバー Scarab [20] を用いて SAT 問題へと符

制約: 各 Vi ∈ {V1 , ..., Vm } について，任意の 2†1 https://github.com/takemaru/graphillion†2 http://www.nysol.jp/apps/ekillion

頂点 u, v ∈ Vi は G 上で連結しなければなら
ない．

v
e

e
e

v
図1

e

e

v

v

ユニバース G

閉路制約が必要となる．これら全ての条件を満たす，
全域部分グラフ G は 2 頂点 v1 と v4 間のパスにな

e

e
v

余分な閉路を含む部分グラフでも解となるため，非v

る (図 2)．

v
図2

e

v

部分グラフ G

この他にも，節 5 で説明するように，ハミルトン閉路問題，k クリーク問題，マルチパス問題などの様々な問題を部分グラフ探索問題として定式化することができる．

• 次数制約 (Degree Constraints)
入力: 頂点から整数集合への写像 f : V → 2N

3 部分グラフ探索問題の制約モデル

制 約: G 上 の 任 意 の 頂 点 v ∈ V に つ い て

本節では，節 2. 1 で説明したグラフ上の制約の有

degG (v) ∈ f (v) が成り立たなければならない．

限整数領域上の制約充足問題としての定式化，すわち

ここで degG (v) は G における頂点 v の次数を制約モデルについて説明を行う．

表す．

• 辺数制約 (Number of Edges)

定式化のための定義を行う．部分グラフ探索問題におけるユニバースを G(V, E) とする．求める全域部

入力: 整数集合 N ⊆ N

分グラフを G(V, E) ⊂ G とし，G を CSP 中で表現

制約: G の辺集合 E について，|E| ∈ N が成りするために，辺集合 E の特性関数を表す以下の変数

立たなければならない．

を導入する．

• 非閉路制約 (No Loop)euv ∈ {0, 1}({u, v} ∈ E)

入力: なしすなわち euv は解となる部分グラフ G を表す変数と制約: G に閉路が含まれてはいけない．

なる．例えば，図 2 のグラフ G は euv によって以下• 候補グラフ集合制約 (Graph Set)のように表される．

入力: 辺集合の集合 {E1 , ..., Em }e12 = 1,

制約: G の辺集合 E について，E ∈ {E1 , ..., Em }以降，特に混乱が生じない時は 0-1 変数を命題変数が成り立たなければならない．

e13 = 0,e23 = 1,e24 = 0,e34 = 1として扱い，¬ ,→ ,∧ ,∨ などの論理演算子と一緒に表記する．例えば euv = 1 および euv = 0 を，それ2. 2 例: パス探索問題

ぞれ euv および ¬euv と表すことがある．

前節で説明した制約を組み合わせることで，これまで研究されてきた様々なグラフ上の問題を部分グ

3. 1 頂点集合制約の制約モデル

ラフ探索問題として定式化することができる． 例

頂点集合制約の入力として頂点集合の集合として，図 1 に示すユニバース V = {v1 , v2 , v3 , v4 }{V1 , ..., Vm } が与えられたとする．Vi の任意の 2 頂と E = {e12 , e13 , e23 , e24 , e34 } が与えられた時に 2 頂点が G において連結している制約を connected(Vi )点 v1 と v4 間のパスを求める問題を考える．この問と表すと，頂点集合制約は以下で記述できる．

題は (i) 頂点集合制約に {{v1 , v4 }} ，(ii) 次数制約に{(v1 , {1}), (v2 , {0, 2}), (v3 , {0, 2}), (v4 , {1})} ，そして (iii) 非閉路制約の 3 つの制約を持つ．頂点集合制
約は 2 頂点 v1 と v4 が G 上で連結しなければならないことを表し，次数制約はパスの始点と終点の次数が 1 であり，その他の頂点の次数は 0 または 2 であることを表している．但し，これらの制約だけでは，∧connected(Vi )i∈{1,..,m}connected(Vi ) の定式化は一般的に難しい．そこ
で，頂点の連結性の推移関係を表す制約 [25] [4] を利用した推移モデルと，頂点の次数制約を利用した新たな次数モデルを実装した．

3. 1. 1 推移モデル

3. 1. 2 次数モデル

2 頂点 s, t が G 上で連結している必要十分条件は，2 頂点 s, t が G で連結している必要十分条件は，

G の全域部分グラフ G′ 上で s, t が連結することで以下を満たす全域部分グラフ G′ (V, E ′ ) ⊂ G が存在ある．まず G′ 上で，s, t が連結する制約を表すためすることである．ただし，degG′ (u) は G′ におけるに，2 つの命題変数を定義する．

u の次数を表す．

auv , avu ∈ {0, 1}({u, v} ∈ E})

ruv ∈ {0, 1}(u, v ∈ V)(u ∈ {s, t})degG′ (u) = 1(u ∈ V \ {s, t})degG′ (u) = 0 or 2

auv , avu は G′ の辺集合 E ′ の特性関数を表す変数で

すなわち，s, t の次数が 1 で，他の頂点の次数が 0あり，各辺に対して双方向に定義される (無向辺を有または 2 である G′ が存在すれば良い．この条件は，向辺と見ることで制約条件を簡潔に記述できるため)．

以下の制約で表現できる (adj(u) は G における u の′

ruv は G 上で，u から v に向かうパスが存在すること

隣接頂点の集合を表す)．ただし e′uv は頂点 s, t と辺を表す変数である．s から t に向かうパスを求めるた{u, v} ∈ E に対し導入された新しい変数であり，G′

めに，rsu (u ∈ V \{s}) に関する制約を記述する (ただの辺集合 E ′ を表す．

し，A = {(u, v) | {u, v} ∈ E} ∪ {(v, u) | {u, v} ∈ E}

e′uv ∈ {0, 1}({u, v} ∈ E)とする)．

e′uv ≤ euv({u, v} ∈ E)

e′uv = 1(u ∈ {s, t})

∑

rst

∨

rsu →

avu

(u ∈ V \ {s})v∈adj(u)((u, v) ∈ A)v∈adj(u)∑{v,u}∈E

auv → rsu

ただし，上式だけでは，閉路の存在を許し，パスが求
まらないことがある．有向閉路を禁止するためには，それぞれの有向辺 (u, v) ∈ A に対して頂点間の連結性の推移関係を表す以下の制約が必要になる．

auv → (ruv ∧ ¬rvu )(auv ∧ rvw ) → ruw(w ∈ V \ {u, v})

最後に， G′ が求める G の全域部分グラフである条
件を記述する．

(auv ∨ avu ) → euv({u, v} ∈ E)

以上が 2 頂点 s, t が G で連結する制約である．この制約を τ (s, t) とすると (τ は trainsition の意)，

e′uv = 0 or 2

こ の 制 約 を δ(s, t) と 表 す (δ は degree の 意)．

connected(Vi ) は以下の連言によって記述できる (但し Vi = {v1 , v2 , ..., vn } とする)．

δ(v1 , v2 ) ∧ δ(v2 , v3 ) ∧ · · · ∧ δ(vn−1 , vn )3. 1. 3 両モデルの変数の数と節数
入力が {V1 , ..., Vm } で与えられた時，節 3. 1. 1 と節 3. 1. 2 で説明した推移モデルと次数モデルの変数の数と節数は以下のようになる．ここで，基数制約∑li=1 xi ≤ k の SAT 符号化節数は O(l · k) と仮定している [18]．また入力の各頂点集合の平均要素数∑
n = ( i |Vi |)/m とする．
変数の数

connected(Vi ) は以下の連言によって記述できる (但し Vi = {v1 , v2 , ..., vn } とする)．

τ (v1 , v2 ) ∧ τ (v2 , v3 ) ∧ · · · ∧ τ (vn−1 , vn )しかし，各 τ (s, t) について，新しく上記の制約を記述する必要はない．つまり， τ (v1 , v2 ) の制約を記述した上で， さらに v1 から t ∈ {v3 , ..., vn } のそれ
ぞれに向かうパスが存在することを表す，次の制約を加えれば良い．

(u ∈ V \ {s, t})

節数

推移モデル

O(m · |V| )O(m · |E| · |V|)

次数モデル

O(m · n · |E|)O(m · n · |E|)2

この表から分かるように，それぞれのモデルの符
号化節数は異なるパラメータに依存していることが分かる．このことから両モデルには得意・不得意な問
題があることが予測できる．節 5 の計算機実験では，
マルチパス問題とハミルトン閉路問題を用いて，両モ∧
t∈{v3 ,...,vn }rv 1 tデルの求解性能を比較する．

3. 2 次数制約の制約モデル

デル

次数制約の入力として頂点から整数集合への写像

論文 [19] では，ハミルトン閉路問題を SAT ソル

f : V → 2N が与えられたとする．この時，次数制約バーを用いて解く方法が提案されている．ハミルトンは次のように定式化できる．
∨∑
euv = d閉路を求めるためのグラフ制約は通常以下の 2 つに(u ∈ V)なる．

• 頂点集合制約: {{V}}d∈f (u) v∈adj(u)• 次数制約: {(v, {2}) | v ∈ V}

3. 3 辺数制約の制約モデル
辺数制約の入力として整数集合 N ⊆ N が与えられたとする．この時，辺数制約は次のように定式化でしかし，論文 [19] では頂点集合制約を記述せずに

CEGAR [3] を使って効果的に問題を解いている．
このような複数のグラフ制約の組合せに対する，制

きる．

∨

∑

約モデルについても実装を行う．具体的な解法は，頂euv = n点集合制約を除いた緩和問題，すなわち次数制約のみ

n∈N {u,v}∈Eで解を求める．その解が頂点集合制約を満たしていな

3. 4 非閉路制約の制約モデル

ければ，解に存在する閉路を否定した制約を加えて，非閉路制約の制約モデルはこれまでいくつか提案されているが [4]，グラフのサイズが大きくなると符号化節数が非常に多くなることが知られている．本研究では非閉路制約は明示的に記述せず CounterExample-

guided abstraction refinement(CEGAR) [3] の手法を用いて，制約を暗黙的に表す．つまり，非閉路制約を除いた緩和問題の解を求め，解に閉路がふくまれていればその閉路を否定する制約を加えて，閉路を頂点集合制約を満たすまで探索を継続する．
今回は頂点集合 {{V}} が与えられた時 (すなわちハミルトン閉路) に限って CEGAR の実装を行った．
非閉路制約と同様に，辺集合で表される k 個の閉路

{E1 , ..., Ek } (k ≥ 2) が解に存在した時，以下の制約を加えながら，頂点集合制約を満たす解が見つかるまで探索を継続する．
∧

含まない解が見つかるまで探索を継続する方法を取る．ある緩和問題の解が辺集合で表される k 個の閉路 {E1 , ..., Ek } を含んでいた場合，以下の制約を加えることにより，これらの閉路を否定する．
∧
∨
¬euv

∨

¬euv

1≤i≤m {u,v}∈Ei

4 SAT ソルバーを用いた部分グラフ探索ツー
ルの実装
本節では，前節で説明したグラフ制約の SAT 符号化を用いた部分グラフ探索ツールの実装について説1≤i≤m {u,v}∈Ei

明する．SAT ソルバーを用いた部分グラフ探索問題

3. 5 候補グラフ集合制約の制約モデル
候補グラフ集合制約の入力として辺集合の集合{E1 , ..., Em } が与えられたとする．候補グラフ集合
制約は以下のように定式化できる．
m
∨
ci
i=1

ci →

∧
{u,v}∈Ei

euv ∧∧の解法の手順は以下になる．

1. 部分グラフ探索問題を 0-1 変数上の CSP として表す．

2. CSP を SAT 問題へと符号化する．
3. SAT 問題を SAT ソルバーを用いて求解し，解¬euv{u,v}∈E\Ei

ここで ci (1 ≤ i ≤ m) は補助命題変数である．

3. 6 複数のグラフ制約の組合せに対する制約モを得る．

4. SAT 問題の解を部分グラフへと変換する．
手順 1 は前節で説明した制約モデルを用いて CSP を構成する．手順 2, 3, 4 については，既存のツール[22] [20] [24] [12] [6] [21] を利用することができる．

今回は，Scala 上に実現された SAT 型制約プログ

表1

ラミングシステム Scarab [20] を基にして，グラフ制

頂点数

問題数

Graphillion

提案方法

約の提案制約モデルを実装した部分グラフ探索ツー

1 - 10026

8

26

101 - 200

23

0

22

201 - 500

37

0

33

ル Scarabellion を開発した．

5 計算機実験k クリーク問題 (k = 3) の求解数

501 - 1000

17

0

10

本節では，k クリーク問題，マルチパス問題，ハミ1001 - 2000

8

0

2

ルトン閉路問題をベンチマークにして提案方法実装

2001 -10000

8

0

0

した部分グラフ探索ツール Scarabellion と既存ツール

合計

119

8

93

Graphillion との比較を行う．
特に頂点集合制約を用いるマルチパス問題，ハミ5. 2 マルチパス問題

ルトン閉路問題については節 3. 1 で説明した推移モ実験の概要：マルチパス問題は長方形のマス目内に数字

デルと次数モデルの比較を行う．ハミルトン閉路にが配置され、同じ数字の間を、縦横の線で重ならない

ついてはこれらの制約モデルに加えて節 3. 6 で説明

ように結ぶ問題であり、電子回路の自動配線と非常にした CEGAR との比較も行う．実験に用いた計算機の CPU は Intel Xeon 3.00GHz でメモリは 16GB で親和性が高い問題である（ナンバーリンクとも呼ばれる †4 ）．頂点集合 S = {s , ..., s } ，T = {t , ..., t }ある．

に対して，頂点のペア (s1 , t1 ), ..., (sn , tn ) のそれぞれ

1

n

1

n

がパスの両端点となるマルチパス問題は以下のグラ

5. 1 k クリーク問題
実験の概要：まず k クリーク問題を用いて Scarabellion

フ制約を用いて部分グラフ探索問題として定式化できる．

と Graphillion の求解性能の比較を行った．k クリー• 頂点集合制約: {{si , ti } | 1 ≤ i ≤ n}

ク問題は以下のグラフ制約を用いて部分グラフ探索• 次 数 制 約:問題として定式化できる．

{(u, {1}) | u ∈ (S ∪ T )} ∪{(u, {0, 2}) | u ∈ V \ (S ∪ T )}• 次数制約: {(v, {0, k − 1}) | v ∈ V}
• 辺数制約: {k(k − 1)/2}
ベンチマーク：ベンチマークにはグラフ彩色問題で使われている color04†3 の 119 個のグラフを使用し，本実験では Graphillion との比較に加えて，頂点集合制約に対する推移モデルと次数モデルの比較も行う．

クリークの次数は k = 3 ，制限時間は 10 分とした．

ベンチマーク：ベンチマークには 2014 年のアルゴリ
ズムデザインコンテスト †5 で使われた 11 問を使用

グラフの頂点数毎の求解数の比較結果を表 1 に示す．

し．制限時間は 60 分とした．それぞれの問題の求解表の列は左から，グラフの頂点数の範囲，その頂点数

時間をと各制約モデルの節数を比較した結果を表 2の範囲にある問題の数，Graphillion の求解数，提案方に示す．

法 (Scarabellion) の求解数を表している．

2 つの制約モデルの比較：まず各制約モデルの符号化求解した問題の大きさと数の比較：表より Graphillion

節数を比較すると，推移モデルが次数モデルより 10はグラフの頂点数が 100 以下の問題しか解けなかっ倍から 100 倍多くなることが分かる．また推移モデ

たことが分かる．一方，提案方法では頂点数が 1000

ルでは NL Q07 以降の問題を制限時間内に符号化す以上になっても 2 問の問題を解くことに成功しておることができなかった．これは節 3. 1. 3 に説明したより，より大きなグラフの問題に対応できていることがうに，推移モデルの符号化節数がグラフの頂点数に大分かる．
†3 http://mat.gsia.cmu.edu/COLOR/instances.html†4 ナ ン バ ー リ ン ク は ニ コ リ 社 に よ る パ ズ ル で あ る(http://www.nikoli.co.jp).
†5 http://www.sig-sldm.org/designcontest.html

表2

マルチパスの求解時間 (秒)提案方法 (求解時間)

提案方法 (節数)問題名

マス目サイズ

線の数

Graphillion

推移モデル

次数モデル

推移モデル

次数モデル

NL Q01

10x10

7

0.1

73.1

12.8

54927511262

NL Q02

10x10

10

0.1

49.9

5.4

78449115778

NL Q03

10x18

9

1.2

546.3

7.3

23130626075

NL Q04

10x18

20

0.1

1146.910.6515733955983

NL Q06

14x18

9

M.O.

T.O.

284.2

460202236806

NL Q07

17x15

13

M.O.

T.O.

T.O.

—

52885

NL Q08

16x19

28

32.46

T.O.

T.O.

—

133155

NL Q0918x18

18147.67

T.O.

55.8

—

92375

NL Q13

18x21

17

M.O.

T.O.

112.4

—

102260NL Q14

18x21

17

M.O.

T.O.

T.O.

—

102260NL Q15

35x19

35

M.O.

T.O.

256.4

—

367143648

求解した問題の合計数
表3ハミルトン閉路問題の求解数

頂点数

問題数

Graphillion

提案方法
推移モデル

次数モデル

CEGAR

1 - 100

23

10

23

17

23

101 - 200

21

0

9

0

18

201 - 500

34

0

5

0

23

501 - 1000

15

0

0

0

5

1001 - 2000

6

0

0

0

1

2001 - 10000

8

0

0

0

0

合計

107

10

37

17

70

きく依存するのに対し，次数モデルでは頂点集合制約

5. 3 ハミルトン閉路問題の入力における集合の要素数に依存することが原因

実験の概要：ハミルトン閉路問題を用いて Graphillion

である．マルチパス問題では入力となる集合の要素数と Scarabellion に実装された 3 つの提案方法，推移モ

は 2 であり，次数モデルが適していると考えられる．

デル，次数モデル，CEGAR の比較を行う．ハミル

求解時間の比較：次に求解時間を比較すると，符号化

トン閉路問題は以下のグラフ制約を用いて部分グラ

節数が少ない次数モデルが推移モデルより多くの問

フ探索問題として定式化できる．

題を高速に解いていることが分かる．また推移モデル• 頂点集合制約: {{V}}は Graphillion と比較しても，多くの問題を解くこと• 次数制約: {(v, {2})|v ∈ V}に成功した．また推移モデルは Graphillion がメモリ

ベンチマーク：実験で用いるグラフは節 5. 1 の k ク

不足により ZDD を構築できなかった最も大きな問題

リークと同様にグラフ彩色問題で使われている color04

である NL Q15 を解くことにも成功した．

のグラフを使用し，制限時間は 10 分とした．ただし，119 個のグラフの中の 12 問については次数が 1 の頂

点を含んでおり明らかにハミルトン閉路を含まないたツール Scarabellion を使ってその性能を評価した．

ので除外し，残りの 107 個のグラフを実験に使用し論文ではまず部分グラフ探索問題とグラフ制約を定た．求解数の結果を表 3 に示す．

義し，その制約モデルを示した．特に頂点集合制約

3 つの制約モデルの比較：表より 3 つの制約モデルでについては推移モデルと次数モデルの 2 つの制約モは CEGAR モデルが最も多くの数の問題と最も大きデルを提案した．k クリーク問題，マルチパス問題，なグラフの問題を解いたことが分かる．次数モデルとハミルトン閉路問題を用いた計算機実験の結果，提推移モデルの比較では，マルチパス問題と異なり推移案方法は ZDD を用いた既存の部分グラフ探索ツール

モデルがより多くの問題を解いた．これは次数モデル

Graphillion より多くの問題，また大きなグラフの問の符号化後の変数の数と節数が，頂点集合制約の入題を解くことができることを確認した．

力となる集合の要素数に大きく依存するためである．

今後の課題は，今回実験した 3 つの問題以外の問

ハミルトン閉路の制約の場合，頂点集合制約の入力は題でも評価を行うことと各制約モデルのさらなる改要素数 |V| 個の頂点集合のみなので，節 3. 1. 3 で述良が挙げられる．また長期的な課題として ZDD とべた推移モデルと次数モデルの変数の数と節数は以SAT の両方を融合した部分グラフ探索方法の研究が下のようになる．

挙げられる．
変数の数

節数

推移モデル

O(|V|2 )O(|E| · |V|)参 考 文 献次数モデル

O(|V| · |E|)

O(|E| · |V|)

[ 1 ] 番原睦則, 田村直之: SAT によるシステム検証, 人
工知能学会誌, Vol. 25, No. 1(2010), pp. 122–129.
[ 2 ] Biere, A., Heule, M., van Maaren, H., andWalsh, T.(eds.): Handbook of Satisfiability, Frontiers in Artiﬁcial Intelligence and Applications(FAIA), Vol. 185, IOS Press, 2009.
[ 3 ] Clarke, E., Grumberg, O., Jha, S., Lu, Y.,
and Veith, H.: Counterexample-guided abstraction
reﬁnement, Computer aided verification, Springer,
2000, pp. 154–169.
[ 4 ] Gebser, M., Janhunen, T., and Rintanen, J.:
SAT modulo graphs: Acyclicity, Logics in Artificial
Intelligence, Springer, 2014, pp. 137–151.
[ 5 ] Hagberg, A. A., Schult, D. A., and Swart, P. J.:
Exploring network structure, dynamics, and function using NetworkX, Proceedings of the 7th Python
in Science Conference (SciPy2008), Pasadena, CA
USA, August 2008, pp. 11–15.
[ 6 ] Hebrard, E., O’Mahony, E., and O’Sullivan,
B.: Constraint Programming and Combinatorial
Optimisation in Numberjack, Proceedings of the
7th International Conference on Integration of AI
and OR Techniques in Constraint Programming for
Combinatorial Optimization Problems (CPAIOR
2010), LNCS 6140, 2010, pp. 181–185.
[ 7 ] 井上克巳, 田村直之: SAT ソルバーの基礎, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 57–67.
[ 8 ] Inoue, T., Iwashita, H., Kawahara, J., and Minato, S.-i.: Graphillion: software library for verylarge sets of labeled graphs, International Journal
on Software Tools for Technology Transfer, (2014),
pp. 1–10.
[ 9 ] Inoue, T., Yasuda, N., Kawano, S., Takenobu,
Y., Minato, S., and Hayashitakeru, Y.: Distribution
Network Veriﬁcation for Secure Restoration by Enu-

この表から分かる通り，変数の数において，次数モデ
ルが推移モデルを上回っているため，次数モデルの求解数が少なくなったと考えられる．実際に，推移モデ
ルが解けて次数モデルが解けなかった 1-Insertions 5(頂点数 202，辺数 1227) の問題では，推移モデルの変数が 44284 個，節数が 1016249 個であったのに対し，次数モデルの変数が 534681 個，節数が 1640367
個と，次数モデルの変数の数が推移モデルに比べて10 倍程度多いことが分かる．さらに，推移モデルで解けて次数モデルで解けなかった 201 頂点以上のグ
ラフ 5 問中 2 問については次数モデルは制限時間内に符号化できなかった．
求解時間の比較：表より 3 つの制約モデルいずれも既存ツールである Graphillion より，多くの問題を解くことに成功した．特に CEGAR モデルでは頂点数が1000 以上のグラフについてもハミルトン閉路を求めることに成功しており，より大きなグラフの問題に対応できていることが分かる．

6 おわりに
本論文では，部分グラフ探索について SAT ソル
バーを用いた新しい解法を提案し，提案方法を実装しmerating All Critical Failures, IEEE Trans. Smart
Grid, Vol. 6, No. 2(2015), pp. 843–852.
[10] Iwashita, H. and Minato, S.: Eﬃcient top-down
ZDD construction techniques using recursive speciﬁcations, Technical Report TCS-TR-A-13-69, Division of Computer Science, Hokkaido University,
2013.
[11] Kawahara, J., Inoue, T., Iwashita, H., and Minato, S.: Frontier-based search for enumerating all
constrained subgraphs with compressed representation, Technical Report TCS-TR-A-14-76, Divisionof Computer Science, Hokkaido University, 2014.
[12] Metodi, A. and Codish, M.: Compiling ﬁnite domain constraints to SAT with BEE, Theory andPractice of Logic Programming, Vol. 12, No. 45(2012), pp. 465–483.
[13] Minato, S.: Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems, DAC, 1993,
pp. 272–277.
[14] 鍋島英知: SAT によるプランニングとスケジューリ
ング, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 114–
121.
[15] 鍋島英知, 宋剛秀: 高速 SAT ソルバーの原理, 人工知能学会誌, Vol. 25, No. 1(2010), pp. 68–76.
[16] Naveh, B. et al.: Jgrapht, Internet: http://jgrapht.
sourceforge. net, (2008).
[17] Siek, J. G., Lee, L., and Lumsdaine, A.: The
Boost Graph Library - User Guide and Reference
Manual, C++ in-depth series, Pearson / Prentice
Hall, 2002.
[18] Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints, Principles
and Practice of Constraint Programming-CP 2005,

Springer, 2005, pp. 827–831.
[19] Soh, T., Berre, D. L., Roussel, S., Banbara, M.,
and Tamura, N.: Incremental SAT-Based Methodwith Native Boolean Cardinality Handling for the
Hamiltonian Cycle Problem, Logics in Artificial
Intelligence - 14th European Conference, JELIA
2014, Funchal, Madeira, Portugal, September 2426, 2014. Proceedings, 2014, pp. 684–693.
[20] Soh, T., Tamura, N., and Banbara, M.: Scarab:
A Rapid Prototyping Tool for SAT-based Constraint Programming Systems, Proceedings of the
16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013),
LNCS 7962, July 2013, pp. 429–436.
[21] Stojadinovic, M. and Maric, F.: meSAT: multiple encodings of CSP to SAT, Constraints, Vol. 19,
No. 4(2014), pp. 380–403.
[22] Tamura, N., Taga, A., Kitagawa, S., and Banbara, M.: Compiling Finite Linear CSP into SAT,
Constraints, Vol. 14, No. 2(2009), pp. 254–272.
[23] 田村直之, 丹生智也, 番原睦則: 制約最適化問題とSAT 符号化, 人工知能学会誌, Vol. 25, No. 1(2010),
pp. 77–85.
[24] Tanjo, T., Tamura, N., and Banbara, M.: Azucar: A SAT-Based CSP Solver Using Compact Order Encoding — (Tool Presentation), Proceedings ofthe 15th International Conference on Theory andApplications of Satisfiability Testing (SAT 2012),
LNCS 7317, Springer, June 2012, pp. 456–462.
[25] Velev, M. N. and Gao, P.: Eﬃcient sat techniques for relative encoding of permutations withconstraints, AI 2009: Advances in Artificial Intelligence, Springer, 2009, pp. 517–527.