米国CMU訪問および国際会議SAT2011参加報告

米国CMU訪問および国際会議SAT2011参加報告
湊 真一
（北海道大学 / JST ERATO）
今回の出張日程


6/18 札幌  成田  Chicago  Detroit (Ann Arbor)
国際会議SAT2011(@Univ. of Michigan)





6/23 Detroit (Ann Arbor)  Pittsburgh
カーネギーメロン大学(CMU)訪問





πDDの論文発表
SAT分野の最新状況調査
ミシガン大の研究室訪問
Bryant教授
Ed. Clarke教授
他6名以上の教授と面会
オバマ大統領来訪
6/25 Detroit  Chicago  成田  札幌 (6/26着)
July 1, 2011
Shin-ichi Minato
2
訪問先の位置関係
- Detroit (Ann Arbor)
- Pittsburgh
米国東部時間（+ サマータイム）
（日本との時差13時間）
（緯度は札幌と仙台の中間）
July 1, 2011
Shin-ichi Minato
3
CMU訪問
July 1, 2011
Shin-ichi Minato
4
CMU訪問の概要

Agenda











6/22昼頃: ピッツバーグ空港着、市内に移動（約1時間）
15:15～ Blanton教授と面会・討論
16:00～ Bryant教授と面会・討論
17:20～ 副研究科長2名（Lehman教授、Sutner教授）と夕食会
6/24 9:30～ Marculescu教授と面会・討論
10:30～ Pfenning教授と面会・討論
11:30～ オバマ大統領の演説を視聴（ストリーミング中継）
12:00～ Theory専攻の教授昼食会にゲスト参加・歓談
13:00～ Sleator教授と面会・討論
14:00～ Ed Clarke教授の研究室でセミナ講演
15:00～ Sutner教授と面会・討論
July 1, 2011
Shin-ichi Minato
5
CMU訪問の概要

- 当初はBryant先生とゆっ
Agenda
くり議論する予定だった。
- オバマ大統領のCMU
 6/22昼頃: ピッツバーグ空港着、市内に移動（約1時間）
来訪が急きょ入ったため、
 15:15～ Blanton教授と面会・討論
Bryant先生は研究科長と
 16:00～ Bryant教授と面会・討論
して演説会場に参列しな
 17:20～ 副研究科長2名（Lehman教授、Sutner教授）と夕食会
ければいけなくなった。
 6/24 9:30～ Marculescu教授と面会・討論
- 私との面会は前日夕方
 10:30～ Pfenning教授と面会・討論
のみに縮小され、代わり
 11:30～ オバマ大統領の演説を視聴（ストリーミング中継）
に多数の有力教授との面
 12:00～ Theory専攻の教授昼食会にゲスト参加・歓談
会・討論をセッティングし
 13:00～ Sleator教授と面会・討論
てくれていた。
 14:00～ Ed Clarke教授の研究室でセミナ講演
 ありがたいことだが、
相当ハードな日程だった。
 15:00～ Sutner教授と面会・討論
July 1, 2011
Shin-ichi Minato
6
Bryant教授とBDD
離散構造の最も基本的なモデルで
ある「論理関数」の処理技法
a
1
簡約化
（圧縮）
0
0
c
1
0
b
a
0
1986年に画期的なBDD演算
アルゴリズムを提案。以後急速
にBDD技術が発達。
（長期間、情報科学の全分野
Bryant (CMU) での最多引用文献となった）
1
b
b
1
c
c
0
1
（BDD）
1
0
1
0
1
BDD
BDD
c
c
0
1
1
（場合分け二分木）
・ 場合分け二分木グラフを簡約化（データ圧縮）
・ 多くの実用的な論理データをコンパクトかつ
一意に表現。（数十～数百倍以上の圧縮率が
得られる例も）
BDD
BDD
AND
BDD
BDD
BDD同士の論理演算
（圧縮データ量にほぼ
比例する計算時間）
近年のPC主記憶の大規模化により、
BDDの適用範囲が拡大
（特に2000年以降）
7
湊とBryant教授との関係
 初めて会ったのは21年前
 湊が初めて国際会議（DAC’90)で発表したとき、
Bryant先生が座長だった。
 たぶん湊より10歳くらい年上
 湊がBDDに関する成果をまとめた
単行本を出版したとき、Bryant先生に
前書きを寄稿していただいた。
 S. Minato: “Binary Decision Diagrams
and Applications for VLSI CAD”
(Kluwer, 1996).
 今回会うのは14年ぶり
 1997年に湊がCMUを訪問して
特別講義をしたとき以来
8
Bryant教授との面会


会うのは14年ぶりだったが、
全くそんな感じがしなかった。
Knuth先生の話で盛り上がる




湊が、最新のπDD と SeqBDD を紹介


Knuth本のBDDのSectionの
お手伝いをされた。
Bryant先生も、Knuth先生の仕事ぶりのすごさにはお手上げ
2人でKnuth本を見ながら重要事項を確認。
非常に興味を持たれていた。
Bryant先生はCMUのCS研究科長（7年目）



5年任期の2期目。多忙なため担当学生は１～２名
講義は持っている。4色問題やTSPを解く学生向けデモプログラム
πDDをそういう有名問題に応用できないかと。（数独とか）
July 1, 2011
Shin-ichi Minato
9
Ed Clarke教授との面会

2007年チューリング賞受賞者




直接お会いするのは初めて


Symbolic Model Checking の考案者
BDDを導入してVLSI検証を実用化
最近はBDD以外にSATやSMTも利用
私がZDDを考案したことはご存知で、ZDDにも興味
湊が、SAT2011発表内容（πDD）を研究室でセミナ講演




ZDDのアイデアから順に説明。よく理解されていた。
πDDの乗算を不動点に達するまで繰り返す手法は、Symbolic
Model Checkingの計算法と似ているので、非常に興味を持たれた。
博士学生にルービックキューブを課題として与えたこともあったそう
で、πDDでの解法に感銘を受けた様子。
Model Checkingの高速化（対称性の除去）にπDDが使えるかも、
とのコメント。関係しそうな論文を渡してくれた。
July 1, 2011
Shin-ichi Minato
10
その他の教授 (1)

Daniel Sleator教授




オンラインアルゴリズム（競合比解析）、探索アルゴリズムが専門。
ゲーム・パズルにも興味。
πDDでルービックキューブを解く話をしたら、とても面白がって、
戸棚からルービックキューブとか様々なパズルが出てきた。
帰って来てから川原さんに聞いたら、オンラインアルゴリズムの大御
所・創始者の1人だったそうで、そうとは知らずに失礼しました。
Klaus Sutner教授


オートマトン解析、群論、計算量、グラフアルゴリズムおよび基盤ソフ
トウェアに興味。πDDとSeqBDDに非常に興味。
昨年、KnuthがCMUに来たときに、自分が考えていた未解決問題を
話したら、1週間後に解けたという手紙が届いたという。現在その話を
論文にまとめているところ。
July 1, 2011
Shin-ichi Minato
11
その他の教授(2)

Shawn Blanton教授



Diana Marculescu教授



VLSIの低消費電力設計が専門。
BDD/ZDDは昔から知っていたが、最近、データマイニングや機械
学習の分野でも応用が広がってると聞いて興味を持っていた。
Frank Pfenning教授



VLSIのテスト生成が専門。
シミュレーション結果を解析して故障診断する手法を研究しており、
LCM over ZDDs の話には興味を持っていた。
論理プログラミング、型理論が専門。ソフトウェアの検証に興味。
第5世代プロジェクトのことを良く知っていた。
Lehman教授

副研究科長。主に産官学連携担当。オバマ訪問の背景を解説して
くれた。
July 1, 2011
Shin-ichi Minato
12
Theory専攻の教授昼食会にゲスト参加・歓談

Theory専攻の教員は週１回の
ランチミーティングで自由に雑談




ホワイトボードに
名前を書いて自己紹介
10数人が参加。ピザ・パスタ・サラダ・
飲み物が置いてあって、自由に取って
食べる。（余った料理は学生に）
この専攻に限らず、CMUは教員同士が
非常に親しく楽しそうなのが印象的
日本の大学の教授会は
もっとお堅い雰囲気だが…
この日の主な話題は



オバマCMU来訪の理由
日本の大震災の様子は？
日本の留学生が最近少ないのは
なぜ？
July 1, 2011
Shin-ichi Minato
13
オバマ大統領のCMU来訪

米国の新しい科学技術プロジェクトを発表（総額600M＄）


CMUで演説したが、全米のトップ大学に共通のプロジェクト



ロボティクスやAIで新規産業を起こし、雇用を創出。
MITの総長も臨席
Stanford, UCB, MIT, U-Michigan, GeorgiaTech 等を列挙
なぜCMUで発表したのか




CMU発のロボティクス分野のスタートアップ企業の実績
ピッツバーグという街の象徴的な歴史（鉄鋼業が寂れた後、ハイ
テク産業で復興、実業中心でリーマンショックのダメージ少ない）
ペンシルベニア州の地政学的重要性（民主党vs共和党）
ワシントンDCから半日往復圏
July 1, 2011
Shin-ichi Minato
14
SAT2011参加報告
July 1, 2011
Shin-ichi Minato
15
SAT2011の概要

開催日程：2011年6月19日（日）～22日（水）





14回目の開催
開催地：Univ. of Michigan （ミシガン大学）
SAT（充足可能性判定問題）およびその発展形
（SMT, CSP, QBF, etc.)の理論と応用に関する
国際会議
Conference Chair:
Karem Sakallah (ミシガン大）
Laurent Simon (パリ南大）
参加者数 約70人
July 1, 2011
Shin-ichi Minato
16
πDDの発表


初日のセッション
SATの会議で、BDDのセッションが１つできた。




「この論文はSATの論文ではなかったけど、とにかく面白かった
から通った」と、Conference Chairが言っていた。
順列空間における制約充足問題という位置づけで、比較的
興味は持ってもらえた。
Symbolic Model Checking の Image computation との
類似性についての質問あり
Symbolic Model Checking がBDDからSATに変わって、
Boundary Model Checking となった経緯があるので、
順列を扱うBDDから、順列を扱うSATに発展する可能性はある。
July 1, 2011
Shin-ichi Minato
17
発表論文の傾向

大きく分類すると




理論の論文が意外と多い


ただし、さほど面白くない物も混じっており、不満を持つ人も。
SATソルバの実装の話はレベルは高いが数は少ない


SATエンジンの中味の実装の話
SATの具体的問題への活用法の話
SATに関する計算量理論の話
簡単には性能向上できなくなっているので、通りにくい
活用手法（変数割り当て, 並列化）は非常に少ない印象


本セッションには落ちて、ポスター発表や併設ワークショップに
回っているものも多い。（PCメンバの趣味？）
特定の応用分野の会議に行かないと通りにくいかも
July 1, 2011
Shin-ichi Minato
18
Best Paper

PCによる査読で3件の候補をノミネート。


学会参加者全員の投票で１件を選出。


理論が２件、実装が１件
実装の論文が選ばれた
“On Freezing and Reactivating Learnt Clauses”
G. Audemard, J. Lagniez, B. Mazure and L. Sais
(Universite Lille-Nord de France)



SATソルバの高速化技術
探索中に値を代入する候補となる項が多数発生するが、どの項
を優先して処理するかを動的に制御する技法を提案
実験結果により有効性を示した。
（ものすごく画期的というほどではない）
July 1, 2011
Shin-ichi Minato
19
個人的に興味を持った論文

“BDDs for Pseudo-Boolean Constraints – Revisited”
I. Abio, R. Nieuwenhuis, A. Oliveras and R.-C. Enric
(Tech Univ. of Catalonia, Barcelona)




主結果：「線形不等式の論理式を表すBDDのサイズは、
NP ≠ co-NP であるとすれば、どんな変数順序でも指数サイズに
なってしまうような係数の組合せが必ず存在する。」
(線形不等式の例) 3x1 + 5x2 + 7x3 < 6
ただし、指数サイズになる組合せの存在を示しているだけで、
指数サイズになる事例を作る構成的な方法は示していない。
（NP ≠ co-NP ならば P ≠ NP が導けるので、たぶん簡単な話で
はなさそう）
係数の総和が小さければ、BDDサイズが小さくなることはKnuth
本で示されている。w1x1 + w2x2 + w3x3+ … < t のとき O((∑w)2）
July 1, 2011
Shin-ichi Minato
20
SAT Competition

毎年開催されているSATソルバの性能コンテスト



首位はppfolioが断トツ




いくつもの部門に分かれて競争
Main track - SAT, UNSAT, SAT+UNSAT
Minisat hack track, 32core track etc.
各部門で順位をつけて、総合点で金銀銅のメダルを授与
ポートフォリオ型（いろんな手法を組み合わせるタイプ）
手法選択の戦略を機械学習するのがウリ
SATソルバ内部に興味を持つ技術者は少々シラケ気味
日本勢も健闘

鍋島先生（山梨大）のGlueMiniSatが複数部門で優勝・入賞



産業応用カテゴリで単一CPUのUNSAT部門で優勝、総合部門(SAT
+UNSAT部門)で2位，単一・複数CPU 全体クラスのUNSAT部門で2位
元々UNSATに特化したツールだが、SATでも意外に強さを発揮
Minisat hack部門で東大稲葉研の学生の園部君が優勝
July 1, 2011
Shin-ichi Minato
21
日本からの参加者と活動状況


今回、本セッションでのacceptは湊だけ
番原先生（神戸大）と学生の丹生さん




ポスターでaccept、併設ワークショップで発表
（SATの変数符号化法の研究）
田村先生（神戸大）代表のSATプロジェクト（基盤A)の中心メンバ。
他に井上克己先生（NII）、岩沼先生、鍋島先生（山梨大）、長谷川
先生、横尾先生（九大）。
日本でほぼ唯一のSATソルバ研究グループ（ただし、始めたのは
割と遅くて2004年頃。元々はSATよりもCSPに興味）
稲葉真理先生（東大）と学生の園部さん、長井先生（群馬大）


併設ワークショップで発表。学生さんがCompetitionで入賞
今井浩先生の研究室出身のグループ
July 1, 2011
Shin-ichi Minato
22
その他のSAT関係者との情報交換

Armin Biere (オーストリア・ケプラー大）


Laurent Simon（パリ南大）


Conf. Co-chair。昔、SATソルバにZDDを使う論文を書いている。
2年前、私がパリ南大に約1カ月滞在していたが、互いに知らなかった。
Karem Sakallah（ミシガン大）


Symbolic Model Checking にSATを導入してBoundary Model Checking とし
て実用化したことで知られる。現在もSAT分野のリーダ的存在。昔、湊のBDDの
本を読んだと言っていた。
Conf. Chair。元はVLSI CAD出身で湊とは知人。πDDに興味。SATの変数対称
性除去の論文を昨年発表していて、関係ありそうなので詳しく説明してくれた。
Igor Markov（ミシガン大）

PCメンバ。湊の知人で北大にも来たことがある。VLSI回路設計の最適化に
BDDやSATを利用。量子回路の設計でも実績。πDDでreversible logicの列挙を
行う方法に非常に興味。30代でミシガン大のテニュア教授獲得。
July 1, 2011
Shin-ichi Minato
23
SAT Conferenceの問題点

PC関係者の論文採択率が他者に比べ大幅に高かった



米国開催なのに欧州からの発表・参加が過半数




日本から少し。中国・インドからゼロ。（MITの中国人留学生1人）
実用的な研究は他の応用分野の学会に流出していると思われる。
欧州の理論研究者の割合が相対的に増加。高齢化。
SAT competitionを続ける意義があるか議論されていた


おそらく投稿数が少なくて、直前にPCに投稿依頼をかけた（と思わ
れる）ことが影響している。（湊の論文IDは締切３日前で8番）
強い新規参入者が少なくなっている。（または技術が深化して、
新規参入者が簡単に成果を出せなくなっている）
今後も続けるが、公平な評価方法と例題設定には不満も
SAT技法は2000年頃に急激に発展したが、今は停滞気味

理論と応用の中間層の実装技術（Art）で、研究コミュニティを保つ
構造的な難しさ。（圧倒的な結果が出続けないと維持できない）
July 1, 2011
Shin-ichi Minato
24
その他の話題

ミシガン大はキャンパスが巨大


最寄りホテルから会場まで約３キロ。学内巡回バスから外れていて、
交通機関なし（徒歩かタクシー）
3日目の午後はバスツアーでデトロイト市内へ





フォードの工場見学（フォードの歴史と最新の製造技術）
フォード博物館
（歴代大統領の公用車、蒸気機関車、飛行機）
（リンカーン奴隷解放に関する記念展示中で大混雑）
GM本社前の河畔公園で記念撮影（対岸はカナダ）
アラブ系アメリカ人記念館でアラブ料理の夕食会
その日の夕方から夜にかけて荒れ模様の天気。
（トルネード警報発令。TVは夜通し速報。シカゴ空港閉鎖で混乱）
July 1, 2011
Shin-ichi Minato
25
その他の写真
July 1, 2011
Shin-ichi Minato
26