MPIによるMinisatの並列化 卒業論文 中間発表 11月30日 塚谷修平 1 研究の対象 • SAT solverの並列化 2 SAT（充足可能判定）問題 • 論理式を充足する変数割り当てが存在す るか • NP完全問題 • 応用分野 – ソフトウェア＆ハードウェア検証 – 自動設計 3 研究の目的 • 数多くのSolverが開発されている – SAT Competition • ソルバの高速化の意義 – 未解決問題の存在 – 更に大規模な問題 • 高速化のアプローチ – 並列化 4 並列SAT solver • 2つのタイプに分類 – OR型並列Solver • • • • 全ての計算ノードがそれぞれ独立に問題を解く いずれかのノードが答えを発見したら終了 MultiSat、MPIzchaff、… 台数性能を発揮するのは困難 – AND型並列Solver • 問題を全ての計算ノードへ分割して解く • 充足可能性をいずれかのノードが発見するか、充足不可能 性を全てのノードが発見する必要性がある 5 OR型並列Solver ノードA 問題 Solver ノードB 問題 Solver ノードC 問題 Solver 各ノードは独立に問題を解く いずれかのノードが答えを発見したら終了する 6 AND型並列Solver 問題を分割し、 各ノードに 振り分ける 問題 Solver Solver ノードA ノードB Solver ノードC 7 AND型並列Solver • 抱える課題 – 負荷分散 • SAT問題は静的な問題分割が困難 • 動的な問題分割が求められる – 通信コスト • 暇なノードが発生しないよう負荷分散し続ける • 問題分割の際の情報共有 8 具体的に目指すもの • 逐次Solverとして優秀なMinisatの並列化 – MPIを用いる – AND型並列Solver • こだわりたい点 – 探索領域の重複なく各ノードに問題を解かせ ることで、UNSATを効率的に判定する実装を 目指す 9 Minisat • DPLLベースのアルゴリズム • 4つのフェーズで構成 – Assume：選択した変数に値を割り当てる – Propagate：Assumeの結果、値が決定できる変数に割 り当てを行い、同時に矛盾が起きてないかチェックを する。 – Analyze：矛盾したClauseを元に、新たなClause（学習 情報）を生成する。また、LearnClauseに依存した Backtrackを行う – Restart：矛盾の回数が一定回数を超えたら、全ての割 り当てを解除する。LearnClauseの数の上限と矛盾数 の上限を増やす。 10 Minisat：Assumeフェーズ • 選択した変数に値を割り当てるフェーズ – Minisat内では、必ず値にFalseを割り当てるよ うにしている – Trueを割り当てても解が変わるわけではない • 並列化する際に、異なる変数割り当てで問題を分 割する事が可能 11 Minisat：Propagateフェーズ • Assumeの次に必ず実行されるフェーズ • 自動的に割り当てが定まる変数に値を割 り当てしていく 例．A = True , B = False , ￢A∨B∨C の時、 C = True と決定する事が出来る • また、矛盾を起こしているClauseがないか どうかチェックをする 12 Minisat : Analyzeフェーズ • 仮にPropagateフェーズで矛盾が検出された場合 に実行されるフェーズ • 矛盾の情報を元に、Learn Clause（学習情報）を 生成する。 • Learn Clauseに依存したバックトラックを行う – 矛盾が起きた場合に、直前の変数割り当てをやり直 すわけではない。この方法は非年代順バックトラックと 呼ばれる 13 Minisat : Restartフェーズ • 矛盾の回数が一定数を超えたら、全ての 変数割り当てを解除する。 – 学習したLearn Clauseを引き継ぐ形で、探索を 初めからやり直す。 • 一度の探索で覚えられるLearn Clauseの数 を制限していて、Restartの度に制限数が増 えていく – Learn Clause数の制限は、変数の数は少ない がそれでいて難しいような問題において重要 14 Minisatのまとめ • C++版とC言語版が存在する – • 1000行程度のプログラムで構成される Learn Clauseの生成、取捨選択が得意 – 探索空間の大幅な削減に貢献 15 Minisatの並列化 • 基本設計 – 管理ノード+計算ノード構造 • 計算ノード – 互いに異なる探索空間を請けおい、Minisatを実行す る • 管理ノード – 計算状態･待機（IDLE)状態の計算ノードを把握する – 全ノードが生産したLearnClauseの管理を行う 16 Minisatの並列化 管理ノード 計算 ノード 計算 ノード 計算 ノード ･･････ 計算 ノード 計算 ノード 17 Minisatの並列化における課題 • どうやって負荷分散をするか – どの方法で計算ノードに問題を振り分けるか • 通信コストをどのように軽減するか 18 並列Minisat：負荷分散 • 変数割り当てによる問題分割が可能 具体的な分割手順 1. ノードAでAssumeフェーズに到達し、変数Zが割り当 て候補として挙がる 2. IDLE状態のノードが無いか探す 3. もしノードBがIDLE状態ならば、「仮にノードAの状 態から変数ZにTrueを割り当てた場合」の探索を ノードBに任せ、ノードAは変数ZにFalseを割り当て た場合の探索を進める 19 並列Minisat：負荷分散 ノードA 通常、Minisatは変数に Falseしか割り当てない。 Z Z = False Z = True 20 並列Minisat：負荷分散 ノードA 探索空間の 削減 Z = False Z Falseを割り当てた結果 Zが矛盾を引き起こすと、 Z=Trueという事を学習し True側の探索空間の 探索を開始する Z = True 21 並列Minisat：負荷分散 ノードA 並列Minisatでは このポイントで問題を 分割する。 Z Z = False Z = True IDLE状態の ノードに任せ る 22 並列Minisat：負荷分散 • 探索域の重複は起こらない • 決めなければならない実装方式 – IDLE状態のノードはどのようにして探すか – ノードAからノードBへ、どの程度の情報を送る べきか 23 並列Minisat：負荷分散 • IDLE状態のノードはどのようにして探すか – 仮に管理ノードを用意しない場合、計算ノードが Assumeフェーズごとに全ノードに問い合わせる？ • 仮に全ノードが探索中であった場合、すぐにはレスポンスが 帰ってこないため、待ち時間が生まれてしまう • ノード数が多くなるほど尋ねるためのコストが増える – 全てのノードのIDLE状態を把握しているノードを用意 する • IDLE状態のノードの有無が、わざわざ全ノードに確認しなく ともに分かる。 • IDLE情報に限らず、全ノード間の必要な情報を管理するノー ドがあると良いのではないか。 → 管理ノード＋計算ノード による並列実装 24 並列Minisat：負荷分散 • 問題の分割を行う際、分割元から分割先 へ送る必要のあるデータは？ – 分割元ソルバに蓄積された情報全て • 問題のサイズによってはメガ単位の情報量になる – 必要な情報の取捨選択が重要 • 最低限必要な情報としては、現在割り当てされて いる値とそれに付随する情報とLearn Clauseが挙 げられる 25 初期状態 ノード1 IDLE ノード2 ノード3 丸は変数割り当てによる 26 探索空間の問題分割 初期状態 ノード１と ノード2の 分岐ポイント ノード1 ノード1 IDLE ノード3 ノード2 27 初期状態 ノード１と ノード3の 分岐ポイント ノード1 ノード1 ノード1 ノード3 IDLE NONE ノード2 ノード2 28 並列Minisat： 計算ノードの終了条件 • 充足可能性の発見 • それ以外には2つのケース – 自身の探索すべき空間の探索終了 – 自身の探索空間を網羅する地点での矛盾を 他ノードが発見 29 並列Minisat： 計算ノードの終了条件 • 自身の探索すべき空間の探索終了 – 探索すべき空間 • 基本的に、自身が問題分割を行ったレベル（探索 木の深さ）の中で直近のレベル以降の探索空間 • 問題分割をした時の直近のレベルの時の相方が UNSATで探索終了済みの場合、探索木をさかの ぼって、相方が探索中なレベルを探す – 仮に見つかったならば、そのレベル以降の探索空間 – 仮に1つも見つからなかった場合、探索木の根以降の探 索空間が探索対象となる 30 初期状態 ノード1 ノード1 ノード1 ノード1の 探索空間 ノード3 IDLE NONE ノード2 ノード2 31 初期状態 ノード1 ノード1 ノード1 ノード3 ノード3の 探索空間 IDLE NONE ノード2 ノード2 32 初期状態 ノード1、2、3 ノード1、3 ノード1 ノード3 IDLE NONE ノード2 ノード1と ノード3の 共通部分 ノード2 33 初期状態 ノード1、2、3 ノード1、2、3 ノード1 矛盾発生！ ノード3との 分岐点まで Backtrack ノード3 IDLE NONE ノード2 ノード2 34 初期状態 ノード2、3 ノード3 ノード3 ノード2 IDLE ノード1 ノード3が未だに 探索状態な場合、 ノード1は探索を 終了させる。 ノード2 35 並列Minisat： 計算ノードの終了条件 • 自身の探索空間を網羅する地点での矛盾を他 ノードが発見 – ノードAがノードBとレベル4（根のレベルは0）にて問題 分割をしたとする。その後、ノードAがノードCとレベル 5にて問題分割をしたとする。仮にAとCが探索中にB がレベル3までバックトラックしたとする。すなわちレベ ル3が原因の矛盾が起きたという事である。レベル3ま での割り当てはA,B,Cが共に同じなので、A,B,Cの全 てが同じ矛盾を持っている事になる。 – つまり、ノードBのバックトラックによってノードAとノー ドCは探索を終了させる事が出来る。 36 初期状態 ノード1、3 ノード1、3 ノード1 矛盾発生！ ノード2との 分岐点まで Backtrack ノード3 IDLE NONE ノード2 ノード2 37 初期状態 ノード2 ノード2 ノード3を跨る バックトラックを行う場合 ノード3も同時に終了 IDLE ノード1 ノード2 ノード2 38 並列Minisat：ソルバの終了 • 逐次版のMinisatは矛盾を重ねるごとに Learn Clauseを蓄積していく – UNSATな問題では、最終的にLearn Clauseの みで矛盾を引き起こしソルバが終了する 39 今後について • 実際に性能が向上するかが未知なので、 早急に実装を行う • 通信コストが及ぼす性能低下も未知なの で、実装が終了しだい詳しく調べてみる 40
© Copyright 2024 ExpyDoc
