SAT技術の進化と応用 〜パズルからプログラム検証まで〜：5. SATソルバーの最近の進展
6
0
0
全文
(2) ❶ マルチエージェントシミ ュレーションの基本設計 SATソルバーの最近の進展. UNSAT. SAT 5,000. Time [sec]. 4,000. 3,000. minisat-2.2.0-simp lingeling-baq. minisat-2.2.0-simp lingeling-baq. glucose-4.0-simp-syrup cominisatps-ms-simp glueminisat-2.2.10-simp. cominisatps-ms-simp glucose-4.0-simp-syrup glueminisat-2.2.10-simp. 2,000. 1,000. 0 200. 250. 300. 350. 400. 450. 500. 200. 250. 300. 350. #Solved. 400. 450. 500. 550. #Solved. 図 -2 SAT 競技会産業応用部門（2012 ～ 2015 年の重複を除く 1,130 問）における求解数と求解時間の分布. 表 す る SAT ソ ル バ ー で あ り，SAT Race 2008. COMiniSatPS. で 優 勝 し て い る． こ の 2008 年 時 点 の 高 速 ソ ル. 18. バ ー MiniSat と 最 新 SAT ソ ル バ ー (Lingeling,. 34. Glucose, COMiniSatPS, GlueMiniSat) と の 性 能 差 を 比 較 し た 結 果 を 図 -2 に 示 す． こ れ は， 過 去 4 年の競技会の産業応用部門の問題群 1,130 問 を 5 種類の逐次ソルバーで解いた結果である. ☆3. ．. MiniSat と 比 較 し て， 最 新 ソ ル バ ー は 充 足 不 能 （UNSAT）な問題の求解能力が飛躍的に向上してい. COMiniSatPS. 24 37. 4. 96. 381 12. 3. MiniSat. 364 3 Glucose. SAT. 2. 6. 1 MiniSat. Glucose. UNSAT. 図 -3 MiniSat, Glucose, COMiniSatPS における求解可能な問題 群の違い. ることが分かる．図中の Lingeling と Glucose もこ の分野を代表する最新ソルバーであるが，MiniSat. えており，SAT の性能が大きく向上していることが. と求解数を比較すると，充足可能（SAT) な問題で. 分かる．なお GlueMiniSat は我々が継続的に開発. は求解数にほとんど変化がないのに対し，UNSAT. しているソルバーであるが，SAT については 20 問. では 100 問程度向上している．この UNSAT の性能. 程度の向上である．. の伸びは，Glucose で導入された単位伝播を促す学. 図 -3 は，MiniSat, Glucose, COMiniSatPS にお. 習節を識別する評価尺度や，良い学習節を求めて頻. ける求解できる問題群の違いを示している．UNSAT. 繁にリスタートする戦略が大きく貢献している．. に関しては，Glucose または COMiniSatPS で求解. さて，SAT に対し最近大きな性能向上を示した. 可能な問題群は，MiniSat で求解可能な問題群をほ. のが COMiniSatPS である．これは Glucose をベ. ぼ包含しており，さらに 100 問程度新たに解ける. ースとして開発されたソルバーであり，2014 年の. ようになっている．一方，SAT に関しては求解に. SAT 競技会で 2 位の SWDiA5BY A26 の後継ソル. 成功した問題群に違いがあり，MiniSat もしくは. バーでもある．図 -2 を見ると，MiniSat, Lingeling,. Glucose のいずれかのソルバーでのみ解けた問題が. Glucose と比較して，SAT の求解数が 40 問程度増. それぞれ約 40 問ある．COMiniSatPS は，MiniSat と Glucose の両者の戦略を取り込んだ戦略を提案. ☆ 3. 実験環境は Core i5 2.3GHz 8GB RAM であり，1 問あたりの制限時 間を 5,000 秒とした．詳細な求解数は表 -2 を参照されたい．. し，一方のソルバーのみが解けていた問題群の大半 を解くことに成功している．その戦略は比較的単純. 情報処理 Vol.57 No.8 Aug. 2016. 725.
(3) 特集. SAT技術の進化と応用〜パズルからプログラム検証まで〜 競技会 SAT Race 2015. ☆6. 1位. 2位. 3位. Glucose. Treengeling. Plingeling. 出場ソルバー数 11 (8p + 3s). SAT Competition 2014. ☆7. Plingeling. PeneLoPe. Treengeling. 14 (10p + 2s + 2h). SAT Competition 2013. ☆8. Plingeling. Treengeling. PeneLoPe. 12 (9p + 2s + 1o). 表 -1 産 業 応 用 部 門 に お け る上位並列 SAT ソルバー. であり，基本的には両者のソルバーの戦略をある間. 間も同じ）を複数の異なる SAT ソルバーによって. 隔ごとに交互に実行するというものである．また，. 並列に解く手法である．. その間隔は繰り返すたびに徐々に拡大する．. 表 -1 は過去 3 年の競技会における産業応用部門に. UNSAT 問題における Glucose 戦略の大きな成功. おける上位並列 SAT ソルバーである．Glucose. はほかのソルバーにも強い影響をもたらし，ほとん. や Plingeling, PeneLoPe が ポ ー ト フ ォ リ オ 型，. どのソルバーが同様の戦略を採用するようになった．. Treengeling が探索空間分割型の並列ソルバーで. COMiniSatPS の貢献の 1 つは，あまり見向きがさ. ある．表中の 8p はポートフォリオ型のソルバーが. れなくなってきていた MiniSat の戦略を見直し，両. 8 種参加したことを意味する．s は探索空間分割型，. 者を活かす戦略を提案したことにある．また SAT. h はポートフォリオと探索空間分割のハイブリッド. に適した戦略と UNSAT に適した戦略とは異なるこ. 型，o はその他（問題の簡単化を並列に行う等）を. とを示した点でも価値がある．. 意味する．競技会では参加ソルバーの大多数がポー. なお我々が開発している GlueMiniSat では，求. トフォリオ型であることが分かる．. ☆5. 解途中に得られる問題の特徴量によって Glucose 風 の戦略が苦手とする問題を識別し，MiniSat の戦略. 探索空間分割型並列 SAT ソルバー. （SAT 向け）または矛盾の導出を促す戦略（UNSAT 向け）に切り替える．これにより SAT, UNSAT の双. 探索空間の分割は，一部の命題変数の真偽値を仮. 方において一定の改善を得ている．. 定することにより行われる．たとえば SAT 問題 P からある変数 x を何らかの基準によって選択し，部. 並列 SAT ソルバー. 分問題 P ∧ x と P ∧¬x に分割する．前者では x を真とした探索空間を，後者では x を偽とした探索. 次に並列 SAT ソルバーにおける最近の話題を紹. 空間を調べることになる．この操作を再帰的に繰り. 介しよう．並列処理により SAT 問題を効率よく解. 返すことにより，探索空間を複数に分割する．. ☆4. の誕生以前から. 図 -4 (a) では，変数 x, y にそれぞれ真偽を割り. 行われていたが，近年の複数の CPU コアを搭載し. 当て，4 つの部分問題を生成している．SAT 問題. た計算機の普及は，それを活用したソルバーの開発. はしばしば数百万変数からなる場合があり，部分. を強く後押ししている．SAT ソルバーの性能を競. 問題の粒度（求解にかかる時間）を小さくするた. う SAT 競技会においても 2008 年より並列ソルバ. めに，より多くの変数の真偽値を仮定したい場合. ー部門が設けられ，継続して実施されている．. がある．図 -4 (b) は (a) と似ているが，S, T はい. 並列 SAT ソルバーには，大別して探索空間分割. くつかのリテラルの連言である．よって部分問題. くための研究は CDCL ソルバー. 型とポートフォリオ型の 2 つがある．前者は，探索 空間を複数に分割し，各部分探索空間を並列に解く. ☆ 5. 手法であり，後者は，同一の問題（すなわち探索空 ☆ 6 ☆ 7 ☆ 4. 726. 本特集「1. SAT 技術の進化」pp.704-709 を参照のこと．. 情報処理 Vol.57 No.8 Aug. 2016. ☆ 8. Glucose はもともと逐次型のソルバーとして開発されていたが，バ ージョン 4.0 よりポートフォリオ型としても動作するように拡張さ れている． http://baldur.iti.kit.edu/sat-race-2015/ http://www.satcompetition.org/2014/ http://www.satcompetition.org/2013/.
(4) ❶ マルチエージェントシミ ュレーションの基本設計 SATソルバーの最近の進展 が必要となる．また，いくつかの変数の真偽値を仮 True. True. False. 定して探索空間を分割したとしても，各部分問題の. False. 探索空間が重複することはままある．分かりやすい 例として 2 つの SAT 問題 P と Q を結合した問題. True. False. P∧Q を考えてみよう．ここで P と Q には変数の 重複がないものとする．部分問題の生成において P 中の変数 x の真偽値を仮定し，部分問題 P∧ x ∧Q. (a) リテラル単位で分割. と P∧ x ∧Q を生成したとする．このとき Q の探 True. 索が重複する．これを避けるためには，各部分問題. False. の求解過程で得られる学習節を交換すればよい．学 True. False. True. False. 習節は探索失敗の記録であり，これを交換すること で同様の探索失敗を別の部分問題の求解において繰. (b) リテラルの連言をもとに分割. り返すことを避けることが可能になる．ただし学習 節の交換にあたっては，それが x に依存せず導出可 能であることを担保する必要がある． 探索空間分割型の SAT ソルバーでは，ある部分 問題において，それを充足する真偽値割り当てが発. (c) 排他的論理和を用いて分割 図 -4 探索空間の分割手法. 見できれば，それは元問題も充足するため SAT と 出力して終了する．逆に UNSAT は，すべての部分 問題が充足不能であると判定された場合となる． さ て， 競 技 会 に お け る 探 索 空 間 分 割 型 並 列 ソ. P∧ S∧T では，(a) よりも多くの変数の真偽値を. ル バ ー の 代 表 例 は Treengeling や Pcasso で あ. 仮定している．ただし S や T はリテラルの選言にな. る．Treengeling は図 -4 (a) のタイプの問題分割. るため，節として追加することになる．たとえば. を，Pcasso は (b) のタイプの問題分割を行う．特に. S=x1 ∧x2, T=y1 ∧y2 と す る と，P∧S∧T で は，. Treengeling は競技会においてもたびたび上位に入. 4 つの変数を真に仮定している．一方 P∧ S ∧T は. 賞する好成績を収めている（表 -1 参照）．. P∧ ( x 1 ∨ x 2) ∧ ( y 1 ∨ y 2) となり，x1 と x2（同様に. Treengeling は，探索空間を分割するための変数. y1 と y2）のうち少なくとも一方が偽となることを. の選択において，先読み型の SAT ソルバーで培わ. 仮定している．図 -4 (c) は排他的論理和を用いた分. れてきた先読み技術を用いて変数を選択し，問題が. 割の例である．部分問題 P ∧ x1 ⊕ x2 ⊕…⊕ xn ⊕ 1. 適当な粒度になるまで再帰的に分割を行い，その後. では，x1, …, xn のうち偶数個の変数が真になるこ. 高速な CDCL ソルバーにより部分問題を並列に解. とを許可し，P ∧ x1 ⊕ x2 ⊕…⊕ xn ⊕ 0 では奇数. く戦略に基づくソルバーである．問題によっては数. 個の変数が真になることを許可している．. 千の部分問題が生成されることもある．先読み型の. 探索空間分割型の SAT ソルバーは，部分問題の. SAT ソルバーでは，ある変数 x に真または偽を割. 生成が比較的容易であるため，大規模並列化に向い. り当てたときに，（x からの単位伝播による割り当. ているといえる．ただし各部分問題の粒度には一般. て等も含めて）充足される節が多くなるような変数. 的に大きなばらつきがあるため，動的な負荷分散（求. を調べて選択する．すなわち問題中の制約（節）が. 解に時間のかかっている部分問題をさらに分割して. 大きく減少するような変数を選択する．変数選択に. 空いているプロセッサに割り当てるなど）の仕組み. は計算コストを要するが，困難な組合せ問題に強い. 情報処理 Vol.57 No.8 Aug. 2016. 727.
(5) 特集. SAT技術の進化と応用〜パズルからプログラム検証まで〜. ことで定評がある．一方，CDCL ソルバーは大規. ソルバー. 求解数 (SAT+UNSAT). 模で比較的容易な SAT 問題を高速に解くことを得. Lingeling-bal. 934 (422+512). 意にしている．先読み型ソルバーにより問題が比較 的容易になるまで再帰的に分割し，その後 CDCL ソルバーにより解くという手法は理にかなっている といえよう． 競技会では共有メモリ型の計算機を用いて評価が. Glucose 4.0. 891 (424+467). COMiniSatPS-MS. 958 (470+488). GlueMiniSat 2.2.10. 968 (450+518). Virtual Best Solver. 1,032 (498+534). 表 -2 SAT 競技会産業応用部門（2012 ～ 2015 年の重複を除く 1,130 問）における求解数. 行われる．CPU コア数は競技会に依存するが 8 ～. 64 コア程度である．探索空間分割型のソルバーは. れすらしないソルバーであった．ppfolio の意図は. 大規模並列化に向いた手法であることを考えると，. 並列ソルバーが達成すべき性能の下限を示すことに. Treengeling はコアの数が限られた環境の中で非常. あったが，はからずもポートフォリオ型の強力さを. に健闘しているといえる．. 示す結果となった． ppfolio はその内部で CryptoMiniSat, Lingeling/ Plingeling, clasp, TNM, Marchi hi という異なる種. ポートフォリオ型並列 SAT ソルバー. 類のソルバーを並列に動作させるが，一方で同じソ. ポートフォリオ型の並列 SAT ソルバーは，同一. ルバーをその探索戦略のパラメータを変えて並列に. の問題を種類の異なる SAT ソルバーで並行して解. 動作させるという手法もよく用いられている．表 -1. くタイプのソルバーである．探索空間分割型とは異. に示した Glucose や Plingeling, PeneLoPe は後者. なり，いずれかのソルバーが SAT または UNSAT を. のタイプの並列ソルバーである．. 検出すれば求解が終了する．. SAT ソルバーには多数のヒューリスティクスが. 表 -2 は，過去 4 年の競技会の産業応用部門の問. たとえば変数選択やリスタートにかかわるヒューリ. 表中の Virtual Best Solver は，4 つのソルバーのう. スティクスのパラメータを変化させた逐次ソルバー. ち 1 つでも解けた場合に「解けた」とカウントした. を複数並列に実行する．ヒューリスティクスは万能. 場合を表す．つまり，1,032 問はいずれかのソルバ. ではないため，多様なヒューリスティクスを並行し. ーを用いることで求解可能であることを示している．. て試すことで相互に補完し合い，安定した性能を獲. よってもし 4 つの CPU コアを搭載した計算機があ. 得することを目指すわけである．またポートフォリ. れば，これらの 4 つのソルバーを並列に実行するこ. オ型では，すべてのソルバーが同一の問題を解くの. とで，いずれの逐次型ソルバーよりも高性能なソル. で，あるソルバーが求解中に獲得した学習節をほか. バーを構成できる．. のソルバーとそのまま共有できる．これにより探索. 題群を 4 種類の逐次ソルバーで解いた結果である. 実際 2011 年の SAT 競技会. ☆ 10. ．. では，大会の運. 空間の重複を避けることが可能になる．ただし学習. 営者が過去の競技会で入賞した複数のソルバーをコ. 節は無数に生成されるため，それを保持するメモリ. ア数に応じて並列実行させるだけの単純なポートフ. や共有にかかわる通信コストを抑えるためにも，良. ォリオ型ソルバー ppfolio を出場させたが，並列部. い学習節を選別することが肝要である．. 門で 7 個のメダルを獲得する猛威を振るった．一般. 逐次 SAT ソルバーとして紹介した COMinSatPS. にポートフォリオ型ソルバーでは探索空間の重複を. では，MiniSat と Glucose の戦略を交互に実行する. 避けるために学習節の交換を行うが，ppfolio はそ. ことで両者の利点を活かしつつ性能向上を達成して. ☆ 9. この結果は図 -2 における求解数をまとめたものである． ☆ 10 http://www.satcompetition.org/2011/. 728. 組み込まれている．ポートフォリオ型ソルバーでは，. ☆9. 情報処理 Vol.57 No.8 Aug. 2016. いる．これは逐次版ポートフォリオとも言えよう． さて，ポートフォリオ型並列ソルバーの利点は，.
(6) ❶ マルチエージェントシミ ュレーションの基本設計 SATソルバーの最近の進展 ppfolio が示したように，コア数が少なくても性能向. 逐次 SAT ソルバーは，1990 年代末に登場した矛. 上が達成しやすいことと，開発が比較的容易である. 盾からの節学習アルゴリズムによって飛躍的にその. 点が挙げられよう．競技会に参加する並列ソルバー. 性能を向上させたが，ここ数年は性能が伸び悩んで. の大多数がポートフォリオ型であることは，これを. いるとの指摘もある．本稿ではそのような状況にお. 裏付けているといえる．一方で課題として大規模並. いても比較的顕著な伸びを示した技術を紹介すると. 列化した場合にスケールするのか，という懸念がある．. ともに，並列 SAT における最近の話題を紹介した．. Baylo らは大規模なクラスタ環境下で動作するポ. もし読者諸氏がこの特集を契機に SAT に興味を持. ートフォリオ型 SAT ソルバー HordeSat を提案し，. ち，逐次版・並列版においてさらなるブレイクスル. 1）. そのスケーラビリティを評価している ．Horde-. ーをもたらしてくれるならば，筆者としては望外の. Sat の構成は比較的単純である．パラメータの異な. 喜びである．. る 16 種類の Lingeling を N 個並列実行する．各ソ ルバーは変数選択時に 1/N の確率でランダムに真 偽値を割り当てる．また各ソルバーは，1 秒ごとに 一定量の学習節（短い節を優先）を全ノードと交換. 参考文献 1） Balyo, T., Sanders, P. and Sinz, C. : HordeSat : A Massively Parallel Portfolio SAT Solver, In Proceedings of SAT 2015 , pp.156-172 (2015). （2016 年 4 月 29 日受付）. する．2,048 ノードからなるクラスタ環境で評価し た結果は，求解に時間のかかる困難な問題において. 1,024 ノードまではほぼ線形に性能が向上すること を示している（その後伸びは鈍る） ．ベースとする ソルバーや環境にも依存すると考えられるが，ポー トフォリオ型の並列ソルバーであっても，かなりの 規模までスケールし得ることを示した点で大変興味 深い．. SAT ソルバーのブレイクスルーを 並列 SAT ソルバーの性能向上には，その基盤と なる逐次 SAT ソルバーの性能向上が不可欠である．. 鍋島英知 [email protected] 山梨大学大学院医学工学総合研究部准教授．博士（工学） ．SAT， プランニング，自動推論等に興味を持つ． 岩沼宏治（正会員） [email protected] 山梨大学大学院医学工学総合研究部教授．工学博士．知能情報学 基礎，特に系列データマイニングや知的推論・学習等に興味を持つ． 井上克巳（正会員） [email protected] 国立情報学研究所情報学プリンシプル研究系教授．総合研究大学 院大学複合科学研究科情報学専攻教授（併任）．東京工業大学情報 理工学研究院情報工学系特任教授．博士（工学）．専門は知能情報学．. 情報処理 Vol.57 No.8 Aug. 2016. 729.
(7)
図
関連したドキュメント
・Squamous cell carcinoma 8070 とその亜型/変異型 注3: 以下のような状況にて腫瘤の組織型が異なると
これはつまり十進法ではなく、一進法を用いて自然数を表記するということである。とは いえ数が大きくなると見にくくなるので、.. 0, 1,
第 5
共通点が多い 2 。そのようなことを考えあわせ ると、リードの因果論は結局、・ヒュームの因果
と言っても、事例ごとに意味がかなり異なるのは、子どもの性格が異なることと同じである。その
FSIS が実施する HACCP の検証には、基本的検証と HACCP 運用に関する検証から構 成されている。基本的検証では、危害分析などの
つまり、p 型の語が p 型の語を修飾するという関係になっている。しかし、p 型の語同士の Merge
本事業を進める中で、
