自動チューニング並列 SAT ソルバ の設計と実装

2010 年度 修士論文
自動チューニング並列 SAT ソルバ
の設計と実装
提出日 : 2011 年 1 月 27 日
指導
: 上田 和紀 教授
早稲田大学大学院基幹理工学研究科
情報理工学専攻
学籍番号 : 5109B053-0
鈴木 宏史
概要
IT 化が進んでいる現代社会では, ソフトウェアの規模の増大やシステム LSI などの
ハードウェアの複雑化が進んでいる. その一方で、これらのソフトウェアやハードウェア
の信頼性の検証には時間がかかり, 検証技術が十分発達しているとは言えない. このよう
な現状の中で, 検証を行うエンジンとして高速化の研究が盛んに行われている分野に充足
可能性問題 (propositional SATisfiability problem, SAT) が挙げられる.
SAT は与えられた命題論理式を充足させるような変数の割り当ての存在の有無を判定
する問題である. 現在, SAT の求解を行う SAT ソルバでは 100 万∼1000 万程度の多数の
変数を持つ問題を扱うことが可能であることと, AI プランニングや回路検証などの問題
が多項式時間内で SAT の問題形式に変換可能なことから検証アプリケーションのエンジ
ンとして SAT ソルバの高速化を行う意義は大きい. また, 大規模クラスタ環境で動作する
並列 SAT ソルバでは多数の CPU を効率的に利用することで逐次 SAT ソルバよりも高速
に求解を行うことが可能になるので, 並列 SAT ソルバの研究も重要である.
本研究では, クラスタ向け並列 SAT ソルバ c-satw を対象とし, 高速化を図ることを目
的とした. c-satw では MiniSAT と PrecoSAT の 2 ストラテジの異なる種類の逐次 SAT
ソルバを連携させることと, 解の探索途中で得る探索域の削減に効果がある学習節を各
ソルバで共有することによって解を高速に求めている. しかし, 並列 SAT ソルバは逐次
SAT ソルバに比べて研究が進んでおらず, 問題に合わせた 2 種類の逐次ソルバの比率や
共有すべき学習節の量の動的な変更は考慮されていない. そこで, これらの要素のチュー
ニングを自動で行うことで更なる高速化を目指す並列 SAT ソルバの作成を行った.
具体的には, 事前に複数の問題について最も求解が速い場合の 2 種類の逐次ソルバの
比率や学習節の共有量を各問題でデータベース化しておき, 未知の問題を解く際にデータ
ベースを利用した機械学習によって各問題での最適な逐次ソルバの割合などを予測・自
動変更することで高速に求解を行わせている. なお, 機械学習としては Support Vector
Machine (SVM) を利用している.
新たに作成した並列 SAT ソルバで SAT-Race 2008 と 2010 の計 141 問について 1200
秒の制限時間を設けて解かせたところ,c-satw に比べて 17% の性能向上を得ることがで
きた.
目次
第1章
はじめに
1
1.1
研究の背景と目的
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1
1.2
論文構成 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2
SAT
3
2.1
SAT の概要 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
2.2
基本用語 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3
2.3
SAT 問題の例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4
2.4
探索アルゴリズム
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
2.5
CDCL アルゴリズム . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5
2.6
データ構造 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
11
SAT ソルバの紹介
13
3.1
逐次 SAT ソルバ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
13
3.2
MiniSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
13
3.3
PrecoSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
14
3.4
並列 SAT ソルバ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15
3.5
c-sat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
16
3.6
c-preco . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
3.7
c-satw . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
Support Vector Machine
20
4.1
機械学習の概要 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
20
4.2
Support Vector Machine の特徴 . . . . . . . . . . . . . . . . . . . . .
20
並列 SAT ソルバ c-satws
25
第2章
第3章
第4章
第5章
i
5.1
c-satws の概要 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
5.2
c-satws の提案理由 . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
5.3
c-satw への SVM の組み込み . . . . . . . . . . . . . . . . . . . . . . .
26
5.4
特徴量の選択 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
27
c-satws のばらつき
28
c-satws における実行時間のばらつき . . . . . . . . . . . . . . . . . . .
28
性能評価
35
7.1
実験環境 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
35
7.2
評価内容 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
36
7.3
予備実験 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
36
7.4
評価実験 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
37
関連研究
40
8.1
AvatarSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
40
8.2
SPEAR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
40
8.3
ManySAT における lemma 共有のチューニング . . . . . . . . . . . . .
41
まとめと今後の課題
42
9.1
まとめ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
9.2
今後の課題 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
第6章
6.1
第7章
第8章
第9章
謝辞
44
参考文献
45
ii
図目次
2.1
CDCL の疑似コード . . . . . . . . . . . . . . . . . . . . . . . . . . . .
6
2.2
resolution による lemma 生成の手順 . . . . . . . . . . . . . . . . . . .
9
2.3
implication graph の例 . . . . . . . . . . . . . . . . . . . . . . . . . .
10
3.1
c-sat, c-preco の階層モデル . . . . . . . . . . . . . . . . . . . . . . . .
17
3.2
c-satw の階層モデル . . . . . . . . . . . . . . . . . . . . . . . . . . . .
19
4.1
SVM の基本的な概念 . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
4.2
ソフトマージン . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
4.3
線形分離が困難な例 . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
4.4
高次元への写像 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
23
4.5
非線形分離の例 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
24
5.1
選択した特徴量 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
27
6.1
gus-md5-09.cnf におけるヒストグラム . . . . . . . . . . . . . . . . . .
30
6.2
q query 3 l44 lambda.cnf におけるヒストグラム . . . . . . . . . . . . .
31
6.3
ACG-20-5p1.cnf におけるヒストグラム . . . . . . . . . . . . . . . . . .
32
6.4
UR-20-5p1.cnf におけるヒストグラム . . . . . . . . . . . . . . . . . . .
32
7.1
SAT instance での性能向上比 . . . . . . . . . . . . . . . . . . . . . . .
38
7.2
UNSAT instance での性能向上比 . . . . . . . . . . . . . . . . . . . . .
39
iii
表目次
6.1
UNSAT instance のばらつき . . . . . . . . . . . . . . . . . . . . . . .
30
6.2
SAT instance のばらつき . . . . . . . . . . . . . . . . . . . . . . . . .
31
6.3
各 instance における t 検定 . . . . . . . . . . . . . . . . . . . . . . . .
33
7.1
実験環境 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
35
7.2
Competitoion 2009 の結果 . . . . . . . . . . . . . . . . . . . . . . . .
36
7.3
Race 2008, 2010 の結果 . . . . . . . . . . . . . . . . . . . . . . . . . .
37
iv
1
第1章
はじめに
1.1 研究の背景と目的
近年, 命題論理の充足可能性問題 (propositional SATisfiability problem, SAT) の求解
を行う SAT ソルバに注目が集まっている. SAT は NP 完全問題であるが, 最新の SAT ソ
ルバでは数百万変数の問題を比較的実用的な数十分で求解を行える点や, AI プランニン
グや回路検証などのツールのエンジンとして SAT ソルバが幅広く利用可能な点から SAT
ソルバの高速化の研究が盛んに行われている. 現在では, マルチコアやクラスタ環境を利
用した逐次 SAT ソルバよりも高速に求解を行える並列 SAT ソルバの開発が行われてい
るが, 並列 SAT ソルバのチューニングによる高速化の研究は進んでおらず, 改良の余地が
大きく残されていると考えられる.
本研究では, 並列 SAT ソルバのチューニングに焦点をあてて高速化を図った. 改良を行
う並列 SAT ソルバとしては現在 SAT ソルバの競技会で公開されている並列 SAT ソルバ
よりも高速に動作する c-satw を選択し, チューニングの手法としては機械学習の 1 種で
ある Support Vector Machine (SVM) を利用した. 機械学習を用いることで手動よりも
コストのかからない自動チューニングを行うことが可能となり, また SVM の特徴である
未知の問題に対する識別能力の高さを活かして自動チューニングによる c-satw の高速化
を目指した.
1.2 論文構成
2
1.2 論文構成
本論文の構成は以下の通りである. 第 2 章では SAT の概要と SAT 問題を解くアルゴ
リズムについて述べる. 第 3 章では本研究での改良対象である並列 SAT ソルバ c-satw を
含めた SAT ソルバの紹介を行う. 第 4 章では Support Vector Machine について述べる.
第 5 章では提案する並列 SAT ソルバについて述べる. 第 6 章では提案する並列 SAT ソ
ルバの評価実験に先立ち, 実行時間のばらつきについて述べる. 第 7 章では提案する並列
SAT ソルバの性能評価実験の結果と考察について述べる. 第 8 章では本研究に関連する
研究について紹介する. 第 9 章では本研究のまとめと今後の課題について述べる.
3
第2章
SAT
本章では, SAT のアルゴリズムについて述べる.
2.1 SAT の概要
充足可能性問題 (SATisfiability problem, 以下 SAT 問題）とは, ある命題論理式全体
が真となるような変数の割り当てが少なくとも一つ存在することを示すか, もしくはその
ような変数割り当ては存在しないことを示す問題である. SAT 問題は NP 完全問題であ
ることが証明されており, 多項式時間内に解を発見することが困難である. そのため, 解の
探索を効率化・高速化する研究が盛んに行われている. また, SAT 問題は AI プランニン
グ, ソフトウェアやハードウェア検証等の検証問題に応用可能であり, これらの基盤エン
ジンとして期待されている.
2.2 基本用語
SAT 問題における専門用語について紹介する.
• 変数 (variable)
論理式を構成する変数. 真または偽の値をとる.
• literal
変数の正または負の出現を表す. ここで正の出現とは否定記号を伴わない変数を、
また負の出現とは否定記号を伴う変数のことを指す.
• clause
literal を論理和で連結した論理式.
2.3 SAT 問題の例
4
• unit clause
cluase に含まれる literal の個数が 1 つのもの. unit clause に含まれる literal は必
ず真となる必要がある.
• binary clause
clause に含まれる literal の個数が 2 つのもの.
• 乗法標準形 (Conjunctive Normal Form, CNF)
clause を論理積で連結した論理式. SAT で扱う問題形式.
• 変数選択 (decision)
未割り当ての変数の中から一つ選び, に真または偽を割り当てる.
• 推論 (deduction)
現在のわかっている変数割り当てから連鎖的な割り当てを行う.
• 衝突 (conflict)
変数割り当てを行った結果, clause が偽となってしまう状態.
• 学習節 (lemma, learned clause)
conflict が起きた際に以降の探索で再び同じ conflict を起こさないために学習する
clause. 特定の探索域に解が存在しないことを表しており解探索の高速化の効果が
ある.
• バックトラック
conflict が起きた場合に decision をやり直すこと.
• activity
変数や clause の優先度・重要度を表す.
2.3 SAT 問題の例
ここでは SAT 問題の例を挙げる. SAT ソルバに与えるために問題は以下のような
CNF で表される.
¶
³
式 1 = (a ∨ b) ∧ (-a ∨ c ∨ d) ∧ (b ∨ −d ∨ e) ∧ (−b ∨ −c ∨ e)
式 2 = (a ∨ b) ∧ (−a ∨ b) ∧ (a ∨ −b) ∧ (−a ∨ −b)
µ
´
これらの例では, () で括られたまとまりが各 clause を, アルファベットが各変数を, アル
ファベットの前の’−’ 記号は変数の負の出現であることを, アルファベットの前に’−’ 記号
2.4 探索アルゴリズム
5
がなければ変数の正の出現をそれぞれ表している.
式 1 を充足 (評価したときに真) させるためには，全ての clause を充足させる変数割り
当てが必要になる．この問題は，a，c，d，e に真を割り当てれば充足可能となる．一方で
式 2 は充足不可能な例として挙げられる．変数 1 と 2 にどのような値を割り当てても，全
ての clause を充足させることはできない．また，充足不可能な問題は，全ての変数に対
して真偽の両方の割り当てを試さなければ判定できない．
2.4 探索アルゴリズム
SAT 問題の探索アルゴリズムは以下の二つに大別される.
• 体系的アルゴリズム
与えられた論理式を充足させるような変数割り当ての方法, または充足不可能であ
ることを示す.
• 確率的アルゴリズム
与えられた論理式を充足させるような変数割り当ての方法のみを示し, 充足不可能
かどうかは示すことができない.
前者の体系的アルゴリズムはヒューリスティックに基づき変数割り当てを行うので , 充
足可能な問題, 充足不可能な問題のどちらにもて適用できる. 一方で後者の確率的アルゴ
リズムはランダムに変数の割り当てを行うので体系的アルゴリズムよりも充足例を早く
発見できるが, 充足不可能であることの証明はできない. 本研究での改良の対象である並
列 SAT ソルバ c-satw では内部で MiniSAT と PrecoSAT という 2 つの逐次 SAT ソルバ
が用いられているが, 両逐次ソルバとも体系的アルゴリズムのソルバに分類される. また,
最近の体系的アルゴリズムの SAT ソルバでは次節で紹介する CDCL (Conflict Driven
Clause Learning) アルゴリズムを採用していることが多く, MiniSAT や PrecoSAT も
CDCL アルゴリズムを採用している.
2.5 CDCL アルゴリズム
近年, 体系的 SAT ソルバで最も用いられる探索アルゴリズムである. Davis, Putnam,
Logemann, Loveland によって考案されたもので当初は DPLL アルゴリズムと呼ばれて
いたが, 最近では lemma (learned clause) を扱いが SAT ソルバの高速化の焦点になって
おり CDCL (Conflict Driven Clause Learning) と呼ばれることが多い. また, このアル
2.5 CDCL アルゴリズム
6
ゴリズムは Davis と Putnam によって考案された DP アルゴリズムを改良したものであ
る. DP アルゴリズムでは使用するメモリが爆発的に増大する問題があったが, この点を
改善し使用メモリ量を抑え, さらにより効率的な探索を行う CDCL アルゴリズムが生み
出された.
CDCL アルゴリズムは以下の 4 つのフェーズから成り立つ.
• decision (変数選択)
• deduction (推論)
• conflict analysis (衝突の解析)
• backtrack (バックトラック)
CDCL アルゴリズムの処理の流れを図 2.1 に示す.
¶
³
CDCL() {
//preprocess()
while(true) {
decision();
status = deduction();
if(status = CONFLICT) {
resolved = conflict_analysis_and_backtrack();
if(!resolved) return UNSATISFIABLE;
conflict_num++;
if(conflict_num reaches to some extent)
restart();
}else if(status = FIND_SOLUTION) {
return SATISFIABLE;
}
}
}
µ
´
図 2.1 CDCL の疑似コード
2.5 CDCL アルゴリズム
7
2.5.1 decision
decision では次に値を割り当てる変数の選択を行い, 選択した変数に真または偽の割り
当てを行う. 現状の変数割り当てだけではこれ以上他の変数の割り当てが定まらない場合
に decision が行われ, まだ値が割り当てられていない変数の中から一つ変数を選び, 真ま
たは偽の値を割り当てる. decision のヒューリスティックスが異なるとそれ以降の探索域
の大きさが大きく異なるので decision のヒューリスティックスが重要となってくる. 現
在, 以下の 3 つが代表的なヒューリスティックスとして考案されている.
• Maximum Occurrences on Minimum sized clauses (MOM)
literal の数が少ない clause に対して，その中で出現頻度の高い literal に優先的に
値を割り当てることで propagation を促進させる手法である．ランダムに作成され
た SAT 問題に対して効果を発揮するものの，構造的な SAT 問題に対して，clause
間の関連する情報を引き出すことができずあまり効果を発揮しない．
• Dynamic Largest Combined Sum (DLCS)
解の探索途中の時点で充足していない clause の中から出現頻度の高い変数を選
択する方法である．この方法では，各変数選択の時点で充足していない clause が
異なるため変数選択の度に計算が必要になり，その計算コストがかかってしまう.
• Variable State Independent Decaying Sum (VSIDS)
与えられた問題に最も多く出現する literal を選択する方法である．lemma の
取得によって clause の数が増えるので，選択する literal は動的に変化する．ま
た,DLCS と異なり変数の選択が変数割り当てに依存しないので，計算コストが抑
えられる．
現在 SAT ソルバの多くは lemma を利用する CDCL アルゴリズムを採用しており, そ
れと合わせて VSIDS が decision のヒューリスティックスと採用される場合が多い.
2.5.2 deduction
deduction では直前の decision での変数割り当てに基づき, 未割り当ての変数に対して
割り当てを行い, その結果として与えられた問題の充足性を判断する. 具体的には, 現在
までの変数割り当てで与えられた問題が充足するか, conflict が起きるか, もしくは充足す
るかしないか不明, の 3 つのどの状態であるかを判断する. 充足する場合は探索を終了し,
2.5 CDCL アルゴリズム
8
conflict が起きた場合は次節で説明する conflict analysis フェーズに進み, 充足するか不
明の場合は次の decision を行う.
長年の研究の結果, いくつかの deduction のアルゴリズムが考案されてきたが, 計算コ
ストが低くさらに探索域を大きく削減することができる unit clause rule というアルゴ
リズムが最も効果的であるとされている. ulit clause rule では, ある clause で一つ以外
の literal が全て偽の割り当てがされていた場合, 残りの literal には必ず真の割り当てを
しないとその clause が充足されなくなる. このような clause は ulit clause と呼ばれ, 全
ての ulit clause に値を割り当てることを unit propagation, または Boolean Constraint
Propagation (BCP) という.
2.5.3 conflict analysis and backtrack
CDCL アルゴリズムでは, conflict が起きた場合にその解析 (conflict analysis) を行い,
バックトラックをして変数割り当てをやり直す. conflict analysis では conflict の原因と
なった変数の割り当ての組みを特定し以降の探索で同じ conflict が起きないように clause
として学習する.
初期の CDCL アルゴリズムでは, 値が割り当てられた変数に対してその変数が真・偽
の両方の値の割り当てが試されたかどうかを示すフラグを用意し, conflict が起きると
真・偽の両方の値の割り当てが試されていない段階まで戻り, 値の割り当てをやりなお
して探索を再開する手法を採用していた. この方法は真・偽両方の値を割り当てが試さ
れていない直近の変数まで backtrack するので chronological backtracking と呼ばれる.
chronological backtracking はランダム生成された SAT 問題に対して効果を発揮する.
chronological backtracking は一方で実アプリケーションから生成される構造的な問
題に対してあまり効果的ではない. そこで conflict が起きると, 直接の原因を解明する
アルゴリズムが考案された. この方式では, 真・偽両方の値の割り当てが試されことの
ない直近の変数の選択よりも前まで戻るので non-chronological backtracking と呼ばれ
る. non-chronological backtracking では conflict analysis の際に conflict の原因を解明
し clause として学習し元の問題に追加される. conflict から学習して clause を得るので,
このような clause を learned clause または lemma と呼ぶ. このとき追加された clause
は元の問題の resolution (図 2.2 参照) により生成されるので与えられた問題の充足性を
変えない. lemma はこの点で冗長であるが特定の探索域に解が存在しないことを表すの
で探索域の削減に役立つので, clause の増加による処理時間の増加とのトレードオフの関
係にある. そのため探索域の削減の効果の高い lemma の学習が重要となる.
2.5 CDCL アルゴリズム
9
¶
³
analyze_conflict(){
cl = find_conflicting_clause();
while(!stop_criterion_met(cl)){
lit = choose_literal(cl);
var = variavle_of_literal(lit);
ante = antecedent(var);
cl = resolve(cl, ante, var);
}
add_clause_to_database(cl);
back_dl = clause_asserting_level(cl);
return back_dl;
}
µ
´
図 2.2 resolution による lemma 生成の手順
以下に lemma の学習方法を述べる. lemma は含意グラフ (implication graph) を基に
して学習される.
• implication graph
implication graph は図 2.3 のように割り当てられた変数の相互関係を示している.
図 2.3 では各ノードは変数, 矢印はエッジを表し, ノードに添えられた括弧内の数
字はそのノードに値が割り当てらたレベル (decision level) を表している. BCP
によって連鎖的な値の割り当てが起きた場合は decision level は等しくなるので,
変数 V11 の割り当てから連鎖的に割り当てが定まった変数は全て decision level
が 5 になっている. 初期の SAT ソルバでは, implication graph を用いなかった
ので conflict が起きるまでに割り当てを行った全ての変数を lemma として学習し
ていたため, 直接 conflict に関係ない変数が含まれており冗長であった. しかし,
implication graph を用いることで decision level を利用した lemma の学習が可能
となっている.
• UIP implication graph において conflict を起こした変数から decision フェーズ
で最後に割り当てた変数までに必ず通過する変数の事. 図 2.3 では変数 V11, V2,
V10 が UIP に相当する.
2.5 CDCL アルゴリズム
10
• First UIP UIP の中で最も conflict を起こした変数に近い UIP を First UIP と呼
ぶ. First UIP でのカットによって生成された lemma が一般的に最も良い性能で
あるとされている. 図??では変数 V10 が First UIP であり, First UIP のカットに
よって生成される lemma は￢ V10, V8, ￢ V17, V19 の否定をとった (V10 ∨ ￢
V8 ∨ V17 ∨ ￢ V19) となり, この clause が元の問題に追加される.
V8(2)
-V6(1)
-V17(1)
V4(3)
-V12(5)
V1(5)
V11(5)
V18(5)
-V2(5)
-V13(2)
-V10(5)
V3(5)
V16(5)
First UIP Cut
-V5(5)
Conflict
-V18(5)
-V19(3)
図 2.3 implication graph の例
このように conflict analysis によって clause の数は増大していく．この追加された
clause は冗長であるため，そのうちのいくつかまたは全てを消去しても，アルゴリズムの
正当性に何も影響を与えることは無い．実際のところ，追加された clause は propagation
を遅延させ，それらを保持し続けることはメモリの負担にもなる．従って，SAT ソルバ
では解の探索において役に立たない clause や，propagation の妨げになる literal を多く
含む clause を削除することで propagation の遅延を減らす工夫が必要となる.
2.5.4 restart
CDCL アルゴリズムを用いた SAT ソルバでは, 類似した問題でも処理時間が大きく変
化する場合が多々ある．例えば, CNF を構成する変数や clause の並び順だけが違う (論
2.6 データ構造
11
理的に等価な) だけでも，処理時間が大変異なるような場合がある．この現象の対処法と
して，random restart の使用が提案されている．これは，ランダムな時間間隔でそれま
での探索域を全て捨て去り最初から探索をやり直す方法である．一見無駄な処理にみえる
が，それまでに得た lemma は保存しているため，それまで調査した探索域を再び探索す
ることは無く，局所解に陥ることを防いでいる．また，探索の初期に行うことで有効な
lemma を学習することができ，SAT ソルバの頑健性の向上にも繋がる．
近年では restart 戦略の研究も盛んに行われており, luby strategy[3] や dinamic restart
などの restart 戦略が考案されている.
2.5.5 subsumption
近年の多くの SAT ソルバでは, subumption と呼ばれる clause の簡略化による clause
データベースの縮小化を行っている. これは clause の個数が多い問題で特に有効であり,
また clause データベースにおける lemma の割合の増大による BCP 効率の低下を引き起
こす問題に対しても MiniSAT などの SAT ソルバで採用されている activity を基にした
lemma の定期的な削減と共に有用である.
2.6 データ構造
現状, SAT solver は数百万の変数や clause を含む問題を扱うことがあるため多量のメ
モリを消費する. さらに解の探索過程において conflict がおきるとその情報を clause の形
で学習するのでメモリ消費量が増える. そこで clause を扱う効率的なデータ構造が必要
となるが, 以下の 3 つの方法が考案されている.
• ポインタを用いる方法
• 配列を用いる方法
• tree 構造を用いる方法
初期の SAT ソルバはポインタを用いてリンクリストの形で clause のデータを扱ってい
た. ポインタを用いると clause のデータの扱いは便利である反面, メモリを効率的に使用
できず, またメモリアクセスの局所性のなさからキャッシュミスが頻繁に発生する問題が
あった.
また, 配列を用いる方法も考案された. 配列を用いて clause のデータを扱う利点は, 配
列が連続したメモリ領域を使用するのでメモリアクセスの局所性が高まりキャッシュミス
2.6 データ構造
12
が減ることである. 一方でリンクリストのような柔軟性がないので, clause の削除の際に
ガーベジコレクションのコードを明示する必要がある.
13
第3章
SAT ソルバの紹介
本章では, 改良を行う対象とした並列 SAT ソルバ c-satw や c-satw の前身である c-sat,
c-preco, またこれらの並列 SAT ソルバで用いられている逐次 SAT ソルバ MiniSAT と
PrecoSAT について紹介する. まず, 逐次 SAT ソルバを紹介し, その後に並列 SAT ソル
バの紹介を行う.
3.1 逐次 SAT ソルバ
現在製作されている多くの SAT ソルバは逐次 SAT ソルバであり, SAT ソルバの性能
を競う競技会の SAT Competition や SAT-Race には毎回多くの逐次 SAT ソルバが出展
されている. 逐次 SAT ソルバの大半は CDCL アルゴリズムを実装しているが, 学習や
restart などのヒューリスティックスやメモリの管理方法などによって性能に大きな差が
ある.
3.2 MiniSAT
MiniSAT は CDCL アルゴリズムを実装した体系的逐次 SAT ソルバであり, SAT
Race 2006, 2008 や SAT Competition 2007 で優秀な成績を収めている逐次 SAT ソル
バである. また, SAT Competition 2009 では MiniSAT hack 部門が新設されるなど,
現在 MiniSAT を基として改良が加えられた逐次ソルバが多数作成されている. また,
ManySAT や PMiniSAT などの並列 SAT ソルバにも MiniSAT が利用されている. c-sat
や c-satw で利用されている MiniSAT は, C 言語約 1000 行で書かれた ver1.14 である.
以下では MiniSAT ver1.14 における CDCL アルゴリズムの説明を行う.
3.3 PrecoSAT
14
3.2.1 decision
MiniSAT では decision のヒューリスティクスとして VSIDS を基にしたヒューリス
ティクスを採用している. decision の際に literal の出現回数である actibity の高い変数
に優先的に割り当てを行う. actibity は literal が conflict に関係した場合に増加されてい
くが, actibity の高い変数は conflict に関係しやすく, BCP 効率が高いと考えれる. その
ため actibity の高い変数に優先的に割り当てを行うことで性能向上を図っている. また,
MiniSAT では 2% の割合で VSIDS ではなくランダム変数選択を行っている.
3.2.2 deduction
MiniSAT では 2-literal watching を採用している. 2-literal watching では各 clause の
先頭 2 つの literal のみを監視するリストを持ち, BCP の際には値が定まった literal に対
してその監視リストに関連する clause をチェックし, 未割り当ての literal が存在する場
合は今値が定まった literal と順番を入れ替え, 常に clause の先頭 2 つの literal が監視の
対象となるように監視リストの更新を行っていく.
3.2.3 conflict analysis
MiniSAT では clause にも activity を持たせてあり, conflict が起きた場合にその原因
となった変数と clause の activity を増加させている. conflict analysis によって得られた
lemma は lemma のみのデータベースに追加される.
3.2.4 restart
MiniSAT はバージョンによって異なる restart 戦略を採用しているが, ver1.14 では
restart の間隔の初期値を conflict 100 回に設定し, restart が発生する度にこの間隔を 1.5
倍に等比的に増加させる手法をとっている.
3.3 PrecoSAT
PrecoSAT は Armin Biere 氏によって作成され, MiniSAT 同様 CDCL アルゴリズ
ムの実装した体系的逐次 SAT ソルバである. PrecoSAT は SAT Competition 2009 の
Application 部門で 1 位を獲得した優秀な逐次 SAT ソルバであり, c-preco や c-satw で
3.4 並列 SAT ソルバ
15
は C++ 言語約 3000 行で書かれた PrecoSAT ver236 が利用されている. PrecoSAT は
Biere 氏が以前に C 言語で作成した PicoSAT をベースにしており, 2 項制約推論等の新
しい機能が追加されている. 以下では PrecoSAT ver236 における CDCL アルゴリズムの
説明を行う.
3.3.1 decision
par PrecoSAT ではバックトラックで割り当てが撤回された変数に優先的に再び割り
当てが行われる. これは MiniSAT における activity の増加と似た効果を持つ. また,
PrecoSAT でもある一定の条件でのランダムな変数選択を行っている.
3.3.2 deduction
Precosat では binary clause 専用のリストを持ち, 初めに binary clause に対して BCP
を行い, conflict が起きなかった場合に 3 以上の長さの clause に対して 2-literal watching
に基づいた propagation を行う. その結果 binary clause になった clause は binary clause
のリストに積まれ, それ以外は MiniSAT 同様監視リストの更新が行われる.
3.3.3 conflict analysis
PrecoSAT では First UIP による lemma の学習が行われる. 学習が行われると,
conflict に最も近いレベルで値が割り当てられた変数に対してその変数の割り当てを反転
させ propagation を行う. その後, lemma に含まれる literal の中で最も浅いレベルで決
定された変数と同じレベルまでバックトラックを行う.
3.3.4 restart
PrecoSAT も MiniSAT 同様 conflict の回数を基準とした restart 戦略を採用してい
る. conflict と探索のレベルが閾値を超えた場合に restart が行われる. conflict の閾値は
luby[3] に基づき, 探索レベルは固定値となっている.
3.4 並列 SAT ソルバ
SAT は lemma の利用によって探索途中で探索域の削減が行われるので探索域の静
的な分割が難しく, また deduction や conflict analysis などのフェーズに要する時間が
3.5 c-sat
16
instance によって様々であるためバランスの良いワークシェアリングを行うことが困難
であり, リニアに近い台数効果は期待しにくい. 現在は lemma の共有による並列効果を
狙う方法が一般的で, 逐次 SAT ソルバの数倍の性能向上を達成している. ただし, 使用す
る PE 数が増加するにつれて lemma 共有に要する時間が増加し, また propagation の速
度の低下も招き易く, 並列 SAT ソルバにおいて効率的な lemma の共有は課題となって
いる.
3.5 c-sat
この節では, クラスタ向け並列 SAT ソルバ c-sat の紹介を行う.
3.5.1 c-sat の概要
c-sat は MiniSAT ver1.14 を基にして Message Passing Interface (MPI) を用いてス
ケーラビリティを考慮したクラスタ向けに並列化された SAT ソルバである. 図 3.1 のよ
うに c-sat は 3 層のマスタ・ワーカ構造をとっている. ワーカは MiniSAT による解の探
索を行い, マスタは各ワーカが探索途中で得た lemma の他のワーカへの配布を行ってい
る. これにより, 各ワーカで lemma を共有することが可能となり, 探索域を効率的に削減
し実行時間を短縮している.
c-sat の性能としては 31PE を利用した状態で, MiniSAT と比較して幾何平均で約 4 倍
の性能向上を達成している.
3.5.2 探索域の変更
c-sat では解の探索はワーカである MiniSAT が請け負っているが, 各ワーカでの探索域
がなるべく重複しないように, ランダムシードの変更する工夫が為されている. MiniSAT
では変数選択の際にヒューリスティック依存選択を 98%, ランダム選択を 2% の割合で
行っているが, ランダムシードを変更することでどちらの変数選択を行うかが変わり, 変
数選択の順番を変えることができる. これにより, 探索域の重複を防ぐことができる.
3.5.3 lemma の共有
lemma は冗長な clause であるが, 探索域の削減に効果があるので lemma の共有は高速
化の有効な手法である. c-sat では lemma の共有は通信を介して行われているので, 共有
3.6 c-preco
17
する lemma が膨大であると通信コストが増大してしまい, 高速化の妨げになってしまう.
そこで, 共有する lemma の量の制限が必要となるが, c-sat では 2 種類の制限を設けてい
る. 一般的に長さの短い lemma のほうが探索域の削減の効果が高く, 有用であると言われ
ているので [2], c-sat では一定値よりも長い学習節は共有しない制限をかけている. しか
し, 探索が進むにつれて取得する学習節は長くなる傾向があるため [5], c-sat では lemma
の平均長に基づく動的な制限値の変更も行っている.
Grandmaster
Grandmaster
lemma exchange
lemma exchange
Childmaster
Childmaster Childmaster
Childmaster
Childmaster
Childmaster Childmaster
Childmaster
lemma exchange
lemma exchange
MiniSAT
MiniSAT
MiniSAT
PrecoSAT
PrecoSAT
PrecoSAT
図 3.1 c-sat, c-preco の階層モデル
3.6 c-preco
次に並列 SAT ソルバ c-preco の紹介を行う.
c-preco は c-sat のワーカ部分を PrecoSAT に変更した並列 SAT ソルバである. マス
タ部分は c-sat と同じ構造をとっている (図 3.1 参照). PrecoSAT は MiniSAT ver1.14
よりも速い逐次ソルバなので, c-preco は c-sat と比較してワーカの性能が向上した並列
SAT ソルバであると言える.
c-preco の性能としては 31PE を利用した状態で, PrecoSAT と比較して幾何平均で約
2.5 倍の性能向上を達成している. 3.7 c-satw
最後に本研究の改良元となった並列 SAT ソルバ c-satw について紹介する.
3.7 c-satw
18
3.7.1 c-satw の概要
c-satw も c-sat と同様のマスタワーカ構造を持つ並列 SAT ソルバであるが, 図 3.2 の
ようにワーカ部に PrecoSAT と MiniSAT の両逐次ソルバを採用するハイブリッド構造
となっている. 基本的な構成としては, 子マスタ 1 台に対して PrecoSAT4 台, MiniSAT1
台の割合となっている. c-satw は lemma 共有の他に PrecoSAT と MiniSAT という異な
る逐次 SAT ソルバを連携によって高速化を達成した並列 SAT ソルバであるが, 以下でこ
の連携の特徴について述べる.
c-satw の性能としては 31PE を利用した状態で, PrecoSAT と比較して幾何平均で約 3
倍の性能向上を達成している.
3.7.2 異なる lemma の共有
MiniSAT と PrecoSAT では衝突の解析に基づく学習のストラテジが異なるため, 取得
する lemma も異なる. そこで, 異なるストラテジから生成された lemma の共有効果が期
待できる.
3.7.3 ストラテジの差異による問題の得手・不得手
また, MiniSAT と PrecoSAT では conflict analysis 以外のストラテジも異なる. 例え
ば, restart のストラテジが異なっている. MiniSAT でも Precosat でも衝突の回数が閾値
を越えた場合に restart を行っているが, 両ソルバではその閾値の設定の仕方が異なって
いる. MiniSAT では, 閾値が等比数列的に増加していくストラテジを採用している. 一方
で PrecoSAT の閾値の設定には, luby ストラテジが採用されている. この違いによって両
ソルバで得意・不得意とする問題が異なってくるが, c-satw では両ソルバを組み込むこと
によって問題の得手・不得手を吸収している.
3.7 c-satw
19
Grandmaster
lemma exchange
Childmaster
Childmaster
Childmaster
Childmaster
lemma exchange
PrecoSAT
PrecoSAT
MiniSAT
図 3.2 c-satw の階層モデル
20
第4章
Support Vector Machine
本章では, 機械学習の一つであるサポートベクターマシン (Support Vector Machine,
SVM) について述べる.
4.1 機械学習の概要
機械学習とは, 人間が行っている学習能力と同様の機能を機械でも実現させるための技
術であり, SVM やニューラルネットワークなどの手法が知られている. 機械学習では、あ
る程度の個数のサンプルデータを解析してそのデータから有用な規則や判断基準などを取
得し利用することを目的としている. 機械学習の手法はロボットをはじめ, 文字や音声認
識などのパターン認識やスパムメールの検出など幅広い分野で利用されている.
機械学習のアルゴリズムは教師ありと教師なし学習に大別できる. 教師あり学習とは,
事前に複数の問題の入力と出力のペア (=教師) が与えられており, それを基にしてある入
力に対する出力を予測するものである. 教師あり学習の例としては SVM や誤差逆伝播法
などがある. 一方で, 教師なし学習では, 事前に教師となるものは与えられず, 多数のデー
タからそれらに共通の規則や特徴を抽出するものである. 教師なし学習の例としては, ク
ラスタリングや主成分分析などが挙げられる.
4.2 Support Vector Machine の特徴
SVM は 1995 年に V.Vapnik が提案した教師ありの学習機械であり, 現在知られている
手法の中で最も識別性能が優れた学習モデルの一つである. SVM の特徴として以下のも
のが挙げられる.
4.2 Support Vector Machine の特徴
21
• 未学習のデータに対する識別能力 (汎化能力) が高い
• 局所最適解に陥らない
• 特徴量によるモデルとクラスの対応付け
• カーネル関数の導入
• マルチクラス分類が可能
まず, 1 つ目と 2 つ目の特徴についてであるが, SVM が登場する前の学習機械では局
所最適解に陥る可能性があるという問題点が存在したが, SVM ではこれを解決している.
SVM の基本的な考え方としてマージン最大化という概念がある. ここで, マージンとは
各クラスに属する要素の中でクラスを分離する分離超平面との最短距離のことを指してい
る (図 4.1 を参照). SVM では, このマージンが最大になるように, つまり 2 クラスのちょ
うど中間でクラスを分けるように分離超平面を決定している. ここで, VC 理論 [17] より
マージンが大きいほど汎化能力が高いことが示されており, マージンが最大になるように
分離超平面を決定する SVM は汎化能力が高いと言える. また, 最大のマージンを求める
際に 2 次の凸計画問題に帰着して求めているが, 2 次の凸計画問題では求めた局所最適解
は大域最適解に等しいという特徴を持つので局所最適解に陥ることを回避している.
2
d
B
d
d
x
A
図 4.1 SVM の基本的な概念
4.2 Support Vector Machine の特徴
22
次に 3 つ目の特徴についてだが, 特徴量というのは各モデルを各クラスに分類するため
の判断基準となるもので, 通常複数の特徴量によって分類を行う. 特徴量の選び方によっ
てはモデルを誤ったクラスに分類する可能性があり, 特徴量の選択は SVM の性能を左右
する重要な要素である.
ただし, 上記のことは線形分離可能であるという前提を基にした議論であることに注意
する必要がある. 現実の問題では, 線形分離可能な場合は少なく, その場合の対策が必要と
なってくる. SVM ではこの対策としてソフトマージンとカーネルトリックの概念を導入
している. まず, ソフトマージンについてだが, これは多少の誤認識を許容するように制限
を緩和する方法である. 分離超平面を超えて他クラス側に存在する要素に対して超越分に
比例するペナルティーを与え, 全ての要素に対するペナルティーの合計が最も小さくなる
ように分離超平面を決定する (図 4.2). ソフトマージンの導入によって線形分離が不可能
な場合においても分類面を決定している.
B
d
d
A
図 4.2
ソフトマージン
しかし, ソフトマージンを用いても図 4.3 のように線形分離が困難な場合が考えられる.
この場合にカーネルトリックと呼ばれる手法で対処している. 一般的に線形分離が不可能
な場合, より高次の空間に写像を行い, その空間で線形分離を行うことが考えられる (図
4.4 参照). これは元の空間で非線形分離を行うことに等しい (図 4.5 参照). この方法には
写像を行う空間の次数が大きい場合やモデルの個数, 特徴量の個数が大きいほど写像にか
4.2 Support Vector Machine の特徴
23
かる計算量が膨大になるという問題点がある. しかし, SVM ではこの計算をカーネル関数
で置き換えてやることで計算量の増大を防いでいる. カーネル関数としては, ガウシアン
カーネルや多項式カーネルなどが知られている. y
B
A
x
図 4.3
線形分離が困難な例
y2
B
x2
A
xy
図 4.4
高次元への写像
4.2 Support Vector Machine の特徴
24
y
B
A
x
図 4.5
非線形分離の例
最後に 5 つ目の特徴についてである. SVM は 2 クラス分類を拡張してマルチクラス分
類を行っている. マルチクラス分類の方法としては, 2 つの方法がある. ここで, クラスの
個数を N としておく. 1 つ目の方法は, N 個の中から 2 つを選んで分類を行う, という操
作を全てのクラスのペアに対して行う方法である. この場合,
N C2
回の分類操作が必要と
なる. 2 つ目の方法は, N 個のクラスから 1 つのクラスを選び, そのクラスとそれ以外のク
ラスで分類を行うという方法である. この場合, N 回の分類操作が必要となる.
25
第5章
並列 SAT ソルバ c-satws
本章では, 提案する自動チューニングを行う並列 SAT ソルバについて述べる.
5.1 c-satws の概要
本研究で提案する並列 SAT ソルバ c-satws では機械学習の一つである SVM を利用し
て自動チューニングを行っている. あらかじめ複数のトレーニングデータから SVM で使
用するデータベースを作成しておき, 問題を解く際にそのデータベースを利用してチュー
ニングを行い, 求解を行っている. 今回はトレーニングデータとして SAT Competition
2009 Application 部門の 292 問を使用している. 5.2 c-satws の提案理由
SAT ソルバの高速化手法の一つにチューニングが挙げられる. しかし, 並列 SAT ソル
バではチューニングの研究はあまり進んでおらず, チューニングによる性能向上の余地が
大きく残っていると考えられる. そこで, 本研究では並列 SAT ソルバのチューニングに焦
点を当てた.
本研究では c-satw を改良を行う対象としたが, c-satw は SAT-Race 2010 のマルチコア
SAT ソルバ部門で最も良い成績を残した plingelinge よりも高速に動作し, 非公開の SAT
ソルバを除いて現状で最速のソルバであるので c-satw を改良の対象として選択した.
c-satw は MiniSAT と PrecoSAT のストラテジの異なる 2 種類の逐次 SAT ソルバを
連携させることで両ソルバの得意・不得意を吸収しているが, ソルバ単体の性能の差から
PrecoSAT を MiniSAT よりも多く使用している. しかし, この PrecoSAT と MinSAT の
5.3 c-satw への SVM の組み込み
26
使用割合は 4:1 で固定されており, この割合を問題毎にチューニングすることでで高速化
が図れると考えた.
5.3 c-satw への SVM の組み込み
c-satw では, 各 PE が親マスタ, 子マスタ, ワーカ (PresoSAT), ワーカ (MiniSAT)
の ど の 役 割 を 分 担 す る か を Message Passing Interface (MPI) で 提 供 さ れ る 関 数
MPI Comm rank() を利用して決めている. MPI Comm rank() は特定のグループの中
において一意に決められる各 PE のランクを取得することができるものである. c-satw で
はこれを利用して役割の分担を行っている.
今回提案する c-satws では, SVM を利用して各 PE が担う役割を instance 毎に変更し
てから解かせるものである.
具体的には SVM を利用するのはランクが 0 の PE である. c-satw では親マスタの個数
は 1 つであり, ランクが 0 の PE がこの役割を担う設計となっている. そこで, ランクが 0
以外の PE に役割を割り振る前にランクが 0 の PE が SVM 用のデータベースと解かせた
い instance の情報を読み込み, その instance を解くのに適した PrecoSAT や MiniSAT
の割合を算出してから各 PE に役割を割り振っている. この役割の割り振りにかかるコス
トは小さく, 数百万の clause の問題において 0.2 秒程度である.
なお, c-satw ではもともと
¶
³
親マスタ 1 台, 子マスタ n 台, PrecoSAT ワーカ 4n 台, MiniSAT ワーカ n 台
µ
´
で構成されているが, 今回の提案手法では上記の他に以下の 3 種類を合わせた 4 種類の構
成のどれかを選択できるようになっている. どの構成の場合でも全体で用いる台数は 31
台で揃えている.
¶
³
親マスタ 1 台, 子マスタ n 台, PrecoSAT ワーカ 3n 台, MiniSAT ワーカ 2n 台
親マスタ 1 台, 子マスタ m 台, PrecoSAT ワーカ 8m 台, MiniSAT ワーカ m 台
親マスタ 1 台, 子マスタ m 台, PrecoSAT ワーカ 7m 台, MiniSAT ワーカ 2m 台
µ
SVM 用のデータベースは SAT Competition 2009 Application 部門の 292 問の各
instance について, どのような PrecoSAT と MiniSAT の使用割合が良いかを表すラベ
´
5.4 特徴量の選択
27
ルとその instance を特徴づける複数の特徴量の組みで構成される. 特徴量は例えば, 各
instance に含まれる変数の個数や clause の個数などが考えられるが, 特徴量の取り方に
よって SVM による分類の精度に大きな影響を与えるので重要となってくる. 次節で今回
選択した特徴量について述べる.
5.4 特徴量の選択
今回使用した特徴量は図 5.1 の 8 種類である. ただし, この 8 種類の中でも SVM の分
類の精度に与える影響の度合いは異なり, 図 5.1 の上の段の特徴量ほど重要な特徴量と
なっている.
例えば, unit clause の個数や clause/変数の割合は instance の大きさに依らず, instance
の種類によって特定の値をとることが多く, unit clause の個数による SVM の分類の効果
が高いと考えられるが, 反対に clause の最小の長さはどの instance でもあまり変わらず,
SVM の分類の効果は低いと考えられる.
¶
³
clause/変数の割合, unit clause の個数
binary clause/clause の割合, clause の最大の長さ
horn clause/clause の割合, 正の literal の個数, 負の literal の個数
clause の最小の長さ
µ
´
図 5.1
選択した特徴量
28
第6章
c-satws のばらつき
本章では, c-satws の実行時間のばらつきに関して述べる.
6.1 c-satws における実行時間のばらつき
一般的に並列 SAT ソルバでは実行時間にばらつきが存在する. c-satws (c-satw も含
む) も例外ではなく, 通信のタイミングによって実行時間がばらつく. 本章では, 実行時間
のばらつきを考慮した上での性能向上比の信頼性についての調査結果を述べる.
6.1.1 正規性の確認
c-satws における実行時間にはばらつきが存在する. これは各ワーカと子マスタ間, 各子
マスタと親マスタ間で lemma 共有の通信を行っているが, この通信のタイミングが実行
毎に異なることが原因である. そのために, 各ワーカが受け取る lemma も実行毎に異なり
探索域が変わってくる. これにより c-satws では実行時間にばらつきが出てくる. 特に解
が複数存在する可能性がある SAT instance においては, 実行毎にどの解を発見するかが
定まらず, 実行時間が大きく変わることが考えられる. これに対して, 解が存在しないこと
を示す UNSAT instance では全探索域を調査する必要があるので, ばらつきはそれほど多
くないことと考えられる.
そこで, c-satw 系列の並列 SAT ソルバの性能評価を行う前にどの程度のばらつきが存
在するのか, またばらつきを考慮した信頼性につてい調査を行った. まずはじめにばらつ
きの分布が正規分布に従うかどうかを調査した. これは, 正規分布に従うかどうかによっ
て, 改良前と改良後のソルバの性能比較の方法が異なるからである. また前述したように
6.1 c-satws における実行時間のばらつき
29
SAT, UNSAT instance で instance の性質が大きく異なるので両者を区別してばらつき
を観察した. 調査対象としては, SAT Competition 2009 の本選の Application 部門から
種類の異なる instance を SAT, UNSAT instance でそれぞれ 10 問ずつ選び, それぞれの
instance を 100 回ずつ解かせ, ばらつきを観察した.
なお, c-satw と c-satws では通信のタイミングに関する変更は行っていないので, c-satw
についてもばらつきに関しては同様の傾向があると考えれる.
正規分布の特徴として, 左右対象の壷形, 平均値から ± 標準偏差分の範囲に約 68%, 平
均値から ± 標準偏差の 2 倍分の範囲に約 95% の割合で分布するという点が挙げられる.
そこで, これらの観点から各 instance が正規分布に従うかどうかを調査した.
まず, UNSAT instance についてであるが, 調査結果を表 6.1 に示す. 表 6.1 は各問題
の平均実行時間, 標準偏差 α, 平均実行時間から ±α 内の分布の個数, 平均実行時間から
2±α 内の分布の個数をまとめたものであるが, どの問題も数値として正規分布に近い値と
なっている. また, 各 instance についてヒストグラムを作成し, グラフから正規分布に近
いかどうかの確認も行った. 作成したヒストグラムの中から 2 つ選んで載せたものが図
6.1 と図 6.2 である. 図 6.1 は gus-md5-09.cnf の, 図 6.2 は q query 3 l44 lambda.cnf の
ヒストグラムであるが, どちらの図も実行時間の平均値を中心として α 分ずつで区切った
の範囲にどれくらい分布しているかを示している. どちらの図においても正規分布に近い
と見做すことができる. 今回示した以外の instance においても分布のヒストグラムは似
たものになり, UNSAT instance ではほぼ正規分布に従っていると見做ことができる.
次に SAT instance についての正規性の確認であるが, 表 6.2 は先の UNSAT instance
と同様に SAT instance の平均実行時間や標準偏差などをまとめたものである. SAT
instance では数値を見ると, 平均値から ±α の中に分布することが多い場合が見受けら
れ, 正規分布に従うと見做すことができるものと, 正規分布に従うと見做せないものの両
方が存在した. また, 各 instance についてヒストグラムを作成したが, 先と同様に 2 つ
載せたのが図 6.3 と図 6.4 である. 図 6.3 は ACG-20-5p1.cnf のヒストグラム, 図 6.4 は
UR-20-5p1.cnf のヒストグラムである. ACG-20-5p1.cnf は正規分布に従うと見做せるが,
UR-20-5p1.cnf は正規分に従うとは見做せない. しかし, UR-20-5p1.cnf のように正規分
布に従うとは見做せないものは少数であり, 全体としてはほぼ正規分布に従うといえる.
6.1 c-satws における実行時間のばらつき
30
instance 名
平均実行時間
標準偏差 α
±α 内の個数
±2α 内の個数
9dlx vliw at b iq1.cnf
117.55
12.95
67
97
ACG-10-5p0.cnf
43.79
1.99
64
97
UCG-15-10p0.cnf
277.63
11.84
70
96
dated-5-15-u.cnf
119.81
6.3
66
94
gus-md5-09.cnf
347.10
15.21
68
97
manol-pipe-c6bidw i.cnf
50.00
1.94
65
93
minand128.cnf
18.42
0.67
66
94
q query 3 l44 lambda.cnf
159.55
10.41
70
95
uts-l06-ipc5-h28-unknown.cnf
31.72
1.22
64
97
velev-live-uns-2.0-ebuf.cnf
10.38
1.16
67
96
表 6.1 UNSAT instance のばらつき
40
35
30
25
20
15
10
5
0
avg-2
avg-2
avgavg
avg
avg
avg+
avg+
avg+2
avg+2
図 6.1 gus-md5-09.cnf におけるヒストグラム
6.1 c-satws における実行時間のばらつき
31
40
35
30
25
20
15
10
5
0
avg-2
avg-2
avgavg
avg
avg
avg+
avg+
avg+2
avg+2
図 6.2 q query 3 l44 lambda.cnf におけるヒストグラム
instance 名
平均実行時間
標準偏差 α
±α 内の個数
±2α 内の個数
9vliw m 9stages iq3 C1 bug5.cnf
26.2
4.7
77
97
ACG-20-5p1.cnf
302.2
16.06
63
93
AProVE09-06.cnf
18.75
10.91
75
92
UCG-15-10p1.cnf
322.31
21.19
67
93
UR-20-5p1.cnf
643.51
89.65
81
92
gss-14-s100.cnf
35.12
2.28
91
94
mizh-sha0-35-3.cnf
35.6
10.63
80
95
partial-10-15-s.cnf
425.54
174.2
66
97
q query 3 L70 coli.sat.cnf
151.59
19.97
71
94
vmpc 30.cnf
62.54
67.87
86
92
表 6.2 SAT instance のばらつき
6.1 c-satws における実行時間のばらつき
32
40
35
30
25
20
15
10
5
0
avg-2
avg-2
avg
avg
avgavg
avg+
avg+
avg+2
avg+2
図 6.3 ACG-20-5p1.cnf におけるヒストグラム
60
50
40
30
20
10
0
avg-2
avg-2
avgavg
avg
avg
avg+
avg+
avg+2
avg+2
図 6.4 UR-20-5p1.cnf におけるヒストグラム
6.1 c-satws における実行時間のばらつき
33
6.1.2 t 検定による有意差の確認
前節より, c-satw と c-satws の実行時間のばらつきがほぼ正規分布に従うと見做すこと
ができると言える. また c-satw と c-satws では解の探索アルゴリズムの変更を行ってい
ないことから両ソルバでの実行時間の分散の度合いは等しいと見做すことができることか
ら, t 検定による平均値の有意差の確認を行った.
instance 名
3回
5回
10 回
9dlx vliw at b iq1.cnf
0.023(34%)
0.001(31%)
0.000(45%)
ACG-10-5p0.cnf
0.029(15%)
0.004(12%)
0.000(15%)
UCG-15-10p0.cnf
0.110(9%)
0.011(9%)
0.000(8%)
dated-5-15-u.cnf
0.003(28%)
0.000(30%)
0.000(33%)
gus-md5-09.cnf
0.013(23%)
0.000(21%)
0.000(23%)
manol-pipe-c6bidw i.cnf
0.000(30%)
0.000(27%)
0.000(27%)
minand128.cnf
0.345(-2%)
0.735(-1%)
0.104(-2%)
q query 3 l44 lambda.cnf
0.004(29%)
0.000(27%)
0.000(25%)
uts-l06-ipc5-h28-unknown.cnf
0.400(6%)
0.445(3%)
0.480(1%)
velev-live-uns-2.0-ebuf.cnf
0.088(35%)
0.002(23%)
0.000(30%)
表 6.3
各 instance における t 検定
表 6.3 は各 instance について c-satw と c-satws について 3, 5, 10 回実行した場合の
t 検定の出力である p 値をまとめたものである. なお, 括弧内の値は c-satw に対する
c-satws の性能向上の割合を表しており, マイナス符号が付いているものは遅くなったこ
とを表している.
t 検定においては, 平均値の差が信頼できるかを判断する基準として有意水準を用いて
いるが, 出力である p 値が 0.05 未満であれば有意水準 5% で 2 つの平均値に差があり,
p 値が 0.01 未満であれば有意水準 1% で 2 つの平均値に差があると言える. 一般的には
5% の有意水準を用いて有意差の有無を示すことが多いが, 表 6.3 より 3 回平均で c-satw
と c-satws を比較した場合でも, 有意水準 5% で有意差があると言える場合が多い. また,
表??の 5 回平均の列をみると, 多くの問題で有意水準 1% でも有意差があると言える. 特
に性能向上の割合が 10% を超えていればほぼ確実に有意差があると言うことができる.
性能向上の割合が 20% を超えていれば確実に有意差があるということができる. この結
6.1 c-satws における実行時間のばらつき
34
果より, 評価実験において性能向上比の値の信頼性を保証するためには, 5 回平均における
評価を行った上で性能向上の割合が 10% を超えていればほぼ有意水準 1% で有意差があ
ると言えると考えられるので 5 回実験を行えばよいと考えられる. 35
第7章
性能評価
本章では, 提案する並列 SAT ソルバ c-satws の性能評価実験について述べる.
7.1 実験環境
本実験で利用した評価実験環境を表 7.1 に示す. なお, 今回の実験では c-satws のマス
タ・ワーカの比率を変更しているが, 使用する PE 数が 31PE で一定となるように変更を
行っている.
CPU
AMD Opteron
周波数
3.0GHz
コア数 (PE 数)
Dual-Core × 8 (16PE)
Node 数
2
メモリ
128GB / Node
通信
10GbE
MPI
MPICH2
SVM
libsvm2.91
表 7.1
実験環境
7.2 評価内容
36
7.2 評価内容
c-satw ではワーカ部の PrecoSAT と MiniSAT の使用割合が固定であった. しかし,
PrecoSAT と MiniSAT で得意とする問題が異なるので, 問題毎にこの割合を動的に変更
することでソルバの高速化が見込まれる. 本実験では, PrecoSAT と MiniSAT の比率を
4:1, 3:2, 7:2, 8:1 の 4 パターンに変更できるようにし, SVM によって問題毎にどのパター
ンを用いるのが適切かを予測し変更をしてから問題を解かせている.
なお, 今回の実験では用いる PE 数を 31PE に揃えるためにこの 4 パターンを採用して
いる. また変更可能なパターンを 4 種類に限定したが, これは変更可能なパターンが多す
ぎると SVM による分類が上手くいかない可能性があるためである.
7.3 予備実験
まず, 予備実験として提案する c-satws でどの程度の性能が出るかを判断するために
SAT Competition 2009 Application 部門の 292 問を解かせた. c-satws で利用するデー
タベースとして上記の instance を用いているので, そのデータベースを使用して同じ
instance を解かせた場合の性能向上を調査することで他の問題を解かせた場合の指標と
することができる. 各 instance の制限時間は SAT Competition で採用されている 1200
秒とし, 制限時間内で解けなかった instance については 1200 秒で解けたと換算している.
予備実験の結果を表 7.2 に示す. なお表中の solved は解けた instance 数, time は総実行
時間で単位は秒となっている.
c-satw
c-satws
solved: SAT
81
83
solved: UNSAT
113
119
solved: TOTAL
194
202
time(s): SAT
13198.8
11189.2
time(s): UNSAT
27268.6
21803.6
time(s): TOTAL
40467.5
32992.8
表 7.2 Competitoion 2009 の結果
7.4 評価実験
37
結果として c-satw に比べて 8 問多く解くことができ, 総実行時間で約 7500 秒短縮する
ことができた. また, 幾何平均で 21% の性能向上を得ており, 他の問題を解かせた場合に
最大で今回と同程度の性能向上が得られると考えられる. この結果を基に以下の評価実験
を行った.
7.4 評価実験
評価実験では, SAT-Race 2008 本選の 100 問と SAT-Race 2010 本選の 100 問の計 200
問の中から予備実験で用いた SAT Competition 2009 の 292 問との重複を除いた 141 問
について c-satws の性能評価を行った. また, 各問題の制限時間は予備実験と同様の 1200
秒に設定し, 1200 秒以内に解けなかった問題については 1200 秒で解けたと換算して性能
向上比を計算した. 評価実験の結果を表 7.3 に示す. なお表中の solved は解けた instance
数, time は総実行時間で単位は秒となっている.
c-satw
c-satws
solved: SAT
44
48
solved: UNSAT
67
69
solved: TOTAL
111
117
time(s): SAT
7036.2
5862.9
time(s): UNSAT
6819.6
5918.4
time(s): TOTAL
13855.8
11781.3
表 7.3 Race 2008, 2010 の結果
結果としては, c-satw と比較して 6 問多く解くことができ, 総実行時間で約 2000 秒の
短縮を達成できた. また, 幾何平均で 17% の性能向上を得ることができた. ここで、性能
向上比 17% という値の信頼性についても言及しておく. 前章でも述べたように c-satw や
c-satws では lemma の共有に通信を用いているが, ワーカと子マスタ間, 子マスタと親マ
スタ間の通信のタイミングが実行毎に異なる. そのため実行毎に各ワーカが得る lemma
が異なり, 実行時間にばらつきが存在する. そこでこのばらつきを考慮した上で性能向上
比の信頼性を考える必要がある. 前章より t 検定において, 性能向上比が 10% ならば有意
水準 1% で信頼性があると言えるとわかっているので, 評価実験結果の 17% という性能
7.4 評価実験
38
向上比においては少なくとも有意水準 1% で信頼性があると言ってよい.
また, SVM を用いた観点からこの結果を見てみると, 予備実験の SAT Competition
2009 を解かせた場合の性能向上比 21% には及ばないものの, 未知の問題である SATRace 2008 と 2010 を解かせた場合の評価実験で 17% の性能向上が得られたので SVM
の汎化能力の高さも確かめられたと言える.
次に SAT instance と UNSAT instance では性質が異なるので, SAT, UNSAT で分け
た上で各 instance 毎の c-satw に対する c-satws の性能向上比についても述べておく. 結
果を 7.1, 7.2 に示す.
c-satw
(s)
図 7.1 SAT instance での性能向上比
まず SAT instace, UNSAT instance に共通して言えることは, 従来の c-satw で実行時
間の短い instance では性能が向上したものと悪化したものが混在しているが, c-satw での
実行時間が 200 秒を超える instance では全ての instance で性能が向上しており, 実行時
間の長い instance で提案手法の効果が高いと言える. SAT instance と UNSAT instance
で異なっている点としては, SAT instance では c-satw での実行時間が長い instance ほど
性能向上比が上昇しているが, これに対して UNSAT instance では c-satw での実行時間
が 100 秒以上の instance に対しては性能向上比が c-satw の実行時間に関係なく 1∼2.5
倍の性能向上が得られている.
7.4 評価実験
39
c-satw
(s)
図 7.2 UNSAT instance での性能向上比
また, 今回は 1200 秒制限で解かせ, 制限時間内に解けなった instance については 1200
秒で解けたとして扱っているので, 図 7.1, 7.2 で c-satw での実行時間が 1200 秒のライ
ンにプロットしてあるものは実際には c-satw で解かせた場合実行時間が 1200 秒以上か
かる instance なので, 性能向上比はさらに上がると考えられる. 上記の結果より, 制限時
間を延ばして実験を行えば, c-satw と c-satws のどちらでも 1200 秒以内で解けなかった
instance についても少なくとも 17% を超える性能向上を得ることができると考えられる.
40
第8章
関連研究
本章では, 本研究と関連のある研究について紹介する.
8.1 AvatarSAT
AvatarSAT[11] は MiniSAT ver2.0 に機械学習を組み込んだ逐次 SAT ソルバである.
AvatarSAT において機械学習によるチューニングを行っているパラメータは restart の
間隔のと変数 activity の増分の 2 種類である. これらのパラメータは MiniSAT の多数の
パラメータの中で性能に大きく影響を与えるものなので, 問題毎に動的に変更させること
でソルバの性能向上が見込まれる.
実際に AvatarSAT では, SAT Competition 2007 と SAT-Race 2008 の中からランダ
ムに選んだ 177 問をトレーニングデータとして利用し, 同競技会からこれもランダムに選
択した 75 問をテストデータとして 12 時間の制限時間で解かせた結果, MiniSAT ver2.0
に比べて幾何平均で 50% の速度向上を達成している.
8.2 SPEAR
SPEAR[12] は定理証明器の一つで内部で SAT ソルバを利用している. この SAT ソル
バでは局所探索法 (local search) によるパラメータのチューニングを行っている. SPEAR
では, decision や clause 削除, restart など 26 種類のパラメータのチューニングを行って
いる.
SPEAR で有界モデル検査の問題で 377 問をトレーニングデータとして利用し, テスト
データとしても 377 題を制限時間 10 時間で解かせたところ, チューニングを行わない場
8.3 ManySAT における lemma 共有のチューニング
41
合に比べて 4.5 倍の速度向上を達成している.
8.3 ManySAT における lemma 共有のチューニング
MiniSAT2.0 を基としたマルチスレッド SAT ソルバ ManySAT[13] の lemma 共有の
チューニングによる高速化の研究. ManySAT ではもともと長さが 8 以下の lemma のみ
を共有する制限が課されているが, この研究では共有する量によって制限長を動的に変更
し, また lemma の activity の高いもののみを共有するように制限の仕方を変更している.
その結果 SAT Competition 2007 crafted 部門の 201 問と SAT-Race 2008 の 100 問の
計 301 問に対して制限時間 1500 秒で解かせたところ, ManySAT に比べて 13 問多く解
くことができている.
42
第9章
まとめと今後の課題
9.1 まとめ
並列 SAT ソルバにおける SVM を用いたチューニングの効果を確認できた. 本研究で
はトレーニングデータとして SAT Competition 2009 のベンチマークを用い, テストデー
タとして SAT-Race 2008, 2010 のベンチマークを使用したが, 選択した特徴量による分
類の精度や SVM の汎化能力の高さによって幾何平均で 17% の性能向上を得ることがで
きた. また, 通信タイミング依存の実行時間のばらつきを考慮した上でも, 性能向上比が
17% であるならば有意水準 1% 以下で信頼性があると言うことができ, 性能向上の信頼性
の確認も行えた.
9.2 今後の課題
9.2.1 他の要素のチューニング
本研究では, 並列 SAT ソルバ c-satw で用いられている 2 種類の逐次 SAT ソルバであ
る PresoSAT と MiniSAT の得手・不得手の違いに着目して, 両逐次 SAT ソルバの使用
比率のチューニングによる高速化を達成した. しかし, 並列 SAT ソルバのチューニングの
分野の研究はあまり進んでおらず改善の余地は多く残されている. 例えば, CDCL アルゴ
リズムの要である lemma の共有に関するチューニングが挙げられる. 並列 SAT ソルバ
では lemma の共有による高速化の効果が大きいが, lemma 共有のための通信コストとト
レードオフの関係にある. そのため, 共有する lemma の量や通信のタイミングのチュー
ニングを行うことで高速化が狙える.
9.2 今後の課題
43
9.2.2 lemma の評価
上記の課題に関連して lemma の評価基準についても課題があると考えられる. 現状
ではどのような lemma が高速化の効果が高いかが明確ではないので, 必ずしも高速化の
効果の高い lemma を共有しているとは言えない. また, 並列 SAT ソルバでは lemma を
共有するので逐次 SAT ソルバよりも多くの lemma を保持するが, lemma を保持しすぎ
ると propagation の速度が下がり結果として実行時間が長くなる弊害がある. そのため,
lemma の良し悪しを評価する明確な基準を定めることでこれらの問題を解決し, 速度向上
を図ることが考えられる.
9.2.3 環境を考慮したチューニング
今回の実験では, 使用する PE 数や通信環境を考慮したものではなく, 他の環境で実験
した場合に同様な速度向上が得られるかの確証はない. そのため, 環境も考慮した上での
チューニングを行うことで, どのような環境でも安定して速度向上を得ることができるよ
うにすることも考えられる.
44
謝辞
本研究を進めるにあたり様々な方の指導・助言をいただきました. まず, ご指導を賜り
ました上田 和紀教授に深く感謝致します. また, SAT のアルゴリズムをはじめ, 研究の相
談にのって頂いた先輩方に深く感致します.
研究対象である c-satw を開発した露崎浩太氏に深く感謝致します.
本研究では，独立行政法人産業技術総合研究所連携検証施設さつきの検証クラスタを利
用させて頂き, 深く感謝致します.
最後に，入学から現在に至るまで，あらゆる面でサポートしてくれた家族に深く感謝致
します.
2011 年 2 月 鈴木 宏史
45
参考文献
[1] Lintao Zhang, Sharad Malik. The Quest for Efficient Boolean Satisfiability
Solvers. 2002.
[2] Armin Biere, Marigin Heule, Hans van Maaren, Toby Walsh. HANDBOOK of
satisfiability. IOS Press. 2009.
[3] Michael Luby, Alistair Sinclair. Optional Speedup of Las Vegas Algorithms. Information Processing Letters. Vol.47,pp.173-180. 1993.
[4] Lintao Zhang, Conor F.Madigan, Matthew H.Moskewicz, Shared Malik. Efficient
Conflict Driven Learning in a Boolean Satisfiability Solver. in Proc of the International Conference on Computer-Aided Design. 2001.
[5] Kei Ohmura, Kazunori Ueda. c-sat: A Parallel SAT Solver for Clusters. SAT’09,
LNCS 5584, pp.525-537, 2009.
[6] 露崎浩太, 村岡崇章, 上田和紀. クラスタ向けハイブリッド SAT ソルバの開発と性能
評価. 情報処理学会第 72 回全国大会. 2010.
[7] Niklas Een, Niklas Sorensson. Minisat: A SAT solver with conflict-clause minimization. In The International Conferrence on Theory and Applications of Satisfiability Testing, 2005.
[8] Niklas Een, Niklas Sorensson. MiniSat Page : http://minisat.sce/
[9] Armin Biere. Pre,icoSAT@SC’09. In SAT 2009 competitive events booklet, pp.4143. 2009.
[10] Roman Gershman, Ofer Strichman. HAIFASAT: A New Robust SAT Solver.
Haifa Verification Conferrence 2005. LNCS 3875, pp.76-89. 2006.
[11] Vijay Ganesh, Rishabh Singh, Joseph.P Near, Martin Rinard. AvatarSAT:An
Auto-tuning Boolean SAT Solver. SAT’09. 2009.
[12] Frank Hutter, Domagoj Babic, Holger H.Hoos, Alan J. Hu. Boosting verification
46
by automatic tuning of decision procedures. In Proceedings of Formal Methods
in Computer Aided Design, pp.27-34. 2007.
[13] Youssef Hamadi, Said Jabbour, Lakhdar Sais. ManySAT: a Parallel SAT Solver.
Journal on Satisfiability, Boolean Modeling and Computation. 2009.
[14] Chih-Chung Chang, Chih-Jen Lin. LIBSVM: a Library for Support Vector Machines. Available: http://www.csie.ntu.edu.tw/ cjlin/libsvm
[15] Chih-Wei Hsu, Chih-Chung Chang, Chih-Jen Lin. A Practical Guide to Support
Vector Classification. Available: http://www.csie.ntu.edu.tw/ cjlin/libsvm
[16] Bernhard E. Boser, Isabelle M. Guyon, Vladimir N.Vapnik. A Training Algorithm
for Optimal Margin Classifiers. In Proceedings of the 5th Annual Workshop on
Computational Learning Theory, pp.144-512. 1992.
[17] Vladimir Vapnik. Statistical Learning Theory. Wiley, New York. 1998.
[18] Youssef Hamadi, Said Jabbour, Lakhdar Sais. Control-based Clause Sharing in
Parallel SAT Solving. In Proceedings of the 21st International Joint Conferrence
on Artificial Intelligence, 2009.
[19] Shai Haim, Toby Walsh. Online Estimation of SAT Solving Runtime. SAT’08,
LNCS 4996, pp.133-138. 2008.
[20] Eugene Nudelman, Kevin Leyton-Brown, Holger H. Hoos, Alex Devkar, Yoav
Shoham. Understanding Random SAT: Beyond the Clauses-to-Variables Ratio.
CP’04, LNCS 3528, pp.438-452. 2004.
[21] Shai Haim, Toby Walsh. Restart Strategy Selection Using Machine Learning
Techniques. SAT’09, LNCS 5584, pp.312-325. 2009.
[22] SAT-Race 2008 : http://www-sr.informatik.uni-tuebingen.de/sat-race-2008/
[23] SAT Competition 2009 : http://www.satcompetition.org/2009/
[24] SAT-Race 2010 : http://baldur.iti.uka.de/sat-race-2010/