決定的ポートフォリオ型並列
SAT
ソルバーの待ち時間削減によ
る高速化手法
Reducing waiting time of deterministic portfolio parallel SAT
solvers
後藤 優也
1鍋島 英知
2∗Yuuya Gotou
1Hidetomo Nabeshima
21
山梨大学大学院医工農学総合教育部工学専攻コンピュータ理工学コース
1
Computer Science and Engineering Course, Faculty of Engineering, Integrated Graduate
School of Medicine, Engineering, and Agricultural Sciences, University of Yamanashi
2
山梨大学大学院医学工学総合研究部
2
Department of Research Interdisciplinary Graduate School of Medicine and Engineering,
University of Yamanashi
Abstract: In this paper, we propose a new method to reduce waiting time in order to improve the
performance of deterministic portfolio parallel SAT solvers. Most of parallel SAT solvers behave non-deterministically, that is, each time solver is executed, it takes different running time in order to decide the satisfiablity, and also it output different satisfying assignment for a satisfiable instance. This non-determinisity brings inconvenience to SAT applications and developers of parallel SAT solvers. On the other hand, the performance of a deterministic parallel solver is inferior to non-deterministic solvers, as it requires synchronization between processes or threads. To reducing waiting time, we propose two techniques: refinement of base interval for synchronization and lazy learnt clause exchange to absorb fluctuation of base interval. Experimental result shows that it can reduce wating time and achieve comparable performance to non-deterministic solvers.
1
はじめに
命題論理式の充足可能性判定問題 (SAT 問題) は，シ ステム検証やプランニング，スケジューリングなどの 産業応用分野で幅広く活用されている．近年 PC のマ ルチコア・メニーコア化が進んでいることから，複数の CPU コアを用いた並列 SAT ソルバーの研究が盛んに 進められている．並列 SAT ソルバーは単一のコア のみ を用いた逐次 SAT ソルバーよりも求解性能がよいため， SAT の応用分野にとって重要である．しかし，既存の 並列 SAT ソルバーのほとんどはその動作が非決定的で あり，実行のたびに求解にかかる時間が異なる，また 充足可能な問題では得られるモデルが求めるたびに異 なるという問題がある．すなわち同じ動作をする再現 性がなく，産業応用分野において扱いづらい一因となっ ている．決定的並列 SAT ソルバーである ManySAT で は，スレッド間で同期をとることで決定的な振る舞い ∗連絡先：山梨大学工学部コンピュータ理工学科 〒 400-8511 山梨県甲府市武田 4-3-11 E-mail: [email protected] を実現しているが，その待ち時間が大きいため非決定 的ソルバーよりも求解性能が低い．そこで本研究では この待ち時間を削減するために，同期までの間隔の精 密化と節交換を遅延させる 2 つの手法を提案する．評 価実験より，本手法によって最新の非決定的並列 SAT ソルバーに匹敵する性能が得られることを実証する．2
SAT
問題と
SAT
ソルバー
SAT とは，与えられた命題論理式を真にする変数割 り当ての存在を判定する問題である．SAT は通常 CNF 式 (Conjunctive Normal Form) で与えられる．命題変 数及びその否定をリテラル，リテラルの選言を節，節 の連言を CNF 式と呼ぶ．節中の 1 つのリテラルのみ が未割り当てで，その他のリテラルが偽の節を単位節 という．SAT 問題を解く SAT ソルバーは，与えられた CNF 式を充足する変数の真偽値割り当てが存在するな らば，充足可能 (SAT) とその真偽値割り当てを出力し， 存在しないならば充足不能 (UNSAT) を出力する． 人工知能学会研究会資料 SIG-FPAI-B509-05この単位節による変数の値割り当てを単位伝播 (unit propagation) と呼ぶ．これを単位節がなくなるまで繰 り返す．単位節が存在しなければ，変数選択ヒューリス ティックスにより変数 x を選択し，x に真または偽を 割り当てる．この変数 x を決定変数と呼ぶ．ある探索 の時点における決定変数の数は探索の深さを表し，こ れを決定レベルと呼ぶ．CDCL はこの単位伝播と変数 選択を繰り返しながら探索を進める．単位伝播処の途 中で，単位節 x と¬x が同時に発生することがある． これを矛盾 (conflict) と呼び，矛盾の原因を解析し同 じ矛盾の発生を防ぐための節を学習する．この節を学 習節という．学習節を元問題に追加することで，過去 に矛盾の原因となった変数割り当ての発生を防ぎ，探 索空間を削減することが可能となる．探索を進めすべ ての節を充足できたならば SAT を返し，網羅的に探索 しても充足可能な割り当てが見つからなかった場合は UNSAT を返す．
2.2
ポートフォリオ型並列 SAT ソルバー
ポートフォリオ型並列 SAT ソルバーは，同一の問題 を複数の異なるソルバーで競争的に解く並列 SAT ソル バーの一種である．各ソルバーは同じ問題を解くが，そ の探索空間の探索順序が異なるため，解の発見が早く なることが期待できる．また求解中に各ソルバーが獲 得した学習節を他のソルバーと交換する．これを学習 節交換または単に節交換という．学習節交換によって 他のソルバーで起きた矛盾と同じ矛盾を繰り返すこと がなくなるので探索が効率化される．すなわち各ソル バーは競争的に解きつつも，協調的に助け合う側面を 持つ．こうして探索を進めていき，どれか 1 つのソル バーが解を発見したら，すべてのソルバーの探索を終 了し，その解を出力する．2.3
決定的・非決定的 SAT ソルバー
与えられた論理式を充足する真偽値割り当てをモデ ルと呼ぶ．一般にモデルはユニークであるとは限らな い．SAT ソルバーが決定的であるとは，充足可能な問 題に対して，同じモデルを見つけることが保証されて いることをいう．非決定的であれば，その保証はない． Glucose [4] などの単一コアの逐次 SAT ソルバーの 殆どは決定的である．決定的なソルバーには利用や評 価がしやすい利点がある．例えばある高速化技法を提 定的である．これは性能向上を重視して，待ち時間が 発生するスレッド間の同期をとることを避けているた めと考えられる．しかし非決定的であることは，並列 ソルバーの開発や各種の技法の評価を難しくする要因 となっている．よって高速な決定的並列ソルバーを開 発することには一定の価値があるといえる． 現在ある並列 SAT ソルバーのほとんどが非決定的な 振る舞いをする要因は学習節交換にある．節交換の手法 はソルバーによって異なるが，ここでは Glucose-Syrup [4] を例に挙げて説明しよう．Glucose-Syrup では節交 換を実現するために，1 つの節交換用の長いキューを用 意しこれをすべてのソルバーで共有する．各ソルバー は矛盾発生時，生成された学習節を他のソルバーに渡 すかどうかソルバーの基準に沿って判断する．学習節 を他のソルバーに渡すとしたとき，先程のキューに学 習節情報を追加する．これを節の export と呼ぶ．これ をすべてのソルバーで行なうことで，キューには交換 する学習節が溜まっていく．そしてソルバーの決定レベ ルが 0 になったときに，キューに溜まった学習節をソル バーに取り込む．これを節の import と呼ぶ．キュー に溜まっている学習節は 1 つのソルバーが節を import してもキューに残ったままで，学習節 C をすべてのソ ルバーが import したら C のみをキューから取り除く． このようにキューを介して学習節の export,import を 行なっている． しかしこの学習節交換は決定的ではない．キューを 共有しているため，どのような順番で学習節が追加さ れていくかは実行するたびに変わる．キュー内の学習節 の順番が違うだけでも，ソルバーは動作が変わるため， この時点でソルバーは決定的ではなくなってしまう．さ らに順番だけでなく，節を import する際にもキューに どれだけ学習節が溜まっているのかは他のソルバーに 依存し決定的ではない．3
ManySAT
ManySAT [5] はポートフォリオ型並列 SAT ソルバー でありながら決定的に動作する SAT ソルバーである． 我々の知る限り唯一の決定的並列 SAT ソルバーである． ManySAT では，探索を period という長さに分割し， 各 period の終了時にスレッド間で同期をとり節交換 を行なうことで決定的な振る舞いを実現している．こ の period は矛盾の発生回数によって定義されている． ManySAT における節交換の概要を次節で紹介する．!" !# $" $# $% $& ' 図 1: ManySAT での period と学習節交換
3.1
ManySAT の節交換手法
コア数を Cores，i 番目のソルバーを Si(0 ≤ i <Cores)，j 番目の period を pj(0≤ j)
と表記する．Pe-riod の長さを矛盾が α 回発生するまでと定義する． ManySAT 2.0 では α = 700 であり，各 period では 700 回の矛盾を起こしている．なお ManySAT 2.0 では period の長さを学習節の数によって動的に [α, 2α] の 範囲で変化をさせているが，ここでは詳細を省略する． 例を図 1 に示す．ここではソルバーごとに 1 period の長さはそれぞれ異なっている．ここで，S1 の p0 と p1の間には空白がある．これは ManySAT ではすべて のソルバーがある時刻 t において同じ period を探索し ていることを要求するためである．もし S1の p0終了 後，すぐに p1に移行してしまうと，S0 よりも先行す ることになる．そのため他のソルバーの p0が終わるま で S1は待つ必要がある．これは他のソルバー・period でも同様であり，各 period ではそれぞれ最も時間がか かるソルバーに合わせて待つ必要がある． 次に学習節交換手法を説明する．ManySAT の学習節 交換の手法は Glucose-Syrup と異なり，各ソルバーが 独自の節交換領域を持ち，この領域は他のソルバーか らの影響を受けない．そのためこの領域への追加は各 ソルバーが独自に行えるため，学習節の export は決定 的に行うことができる．節の import では，各 period pi から pi+1 に移行する際に各ソルバーから節を取り 込む．すべてのソルバーが piの探索を終えたら，各ソ ルバーは他のソルバーが piで獲得した学習節を節集合 に追加する．import する学習節とその順序は決定的で あるのでソルバー全体の決定性は維持される．
3.2
ManySAT の問題点
ManySAT は節交換のタイミングを決定的にするこ とで決定性を維持しているが，そのために各ソルバー は節交換時に同期を取るための待ち時間が発生してし まう．待ち時間の間はソルバーは停止しており，長い 待ち時間は求解性能を低下させる要因となる． ManySAT における求解時の待ち時間と，それによ る求解性能低下の度合いを調べるため予備実験を行っ た．ただし ManySAT 2.0 は MiniSat をベースに開発 0.4 0.5 0.6 0.7 0.8 0.9 1 0 100 200 300 400 500 600 700 runtime/realtime instances manysat 図 2: ManySAT 手法の実行時間の割合 されたものであり，最新 SAT ソルバーよりも性能が非 常に低い．そのため ManySAT の決定的節交換手法を， 最新のソルバーである Glucose-Syrup 4.1 に移植し実 験を行った．節交換領域を各ソルバーに独自に持たせ ることで排他的な利用を可能とし，どの学習節を交換 するのかは Glucose-Syrup の節交換の基準に従う．実験環境は CPU Intel Core i5-6600 (3.30GHz)，4 コア，14GB RAM であり，評価用問題群として SAT Competition, SAT-Race 2014-2016 Application 部門 の重複を除く全 745 問を使用した．制限時間は１問あ たり 5000 秒である． 待ち時間がどのくらいあるのか検証を行なう．ここ で待ち時間 (waiting time) とは同期待ちの時間を指し， 実行時間 (runtime) とは CPU が実際に走っている時間， つまり同期待ちではない時間を指し，実時間 (realtime) とは実際に掛かった時間で実行時間と待ち時間の合計 である．結果を図 2 に示す．この図は実行時間の割合 (runtime / realtime) を示している．図より，745 問中 およそ 500 問は待ち時間の割合が 10%以上を占めてお り，さらにその内 200 問ほどは待ち時間の割合が 20%以 上を占めていることが分かる．この待ち時間は決定的 にするために同期待ちをしている時間で，ソルバーに はそれだけ無駄があるということになる． 次に求解数，求解時間の比較を行なう．比較対象は， ベースとした非決定的並列ソルバーの Glucose-Syrup であり，これを 10 回実行しその平均と比較する．なお， 決定的 SAT ソルバーでは何回実行しても同様の探索順 で探索を行なうが，乱数の seed 値によっては実験結果 に大きく差が出ることがある．seed 値の違いによる実 験結果の差は本質的ではないため，seed 値を 5 つ用意 して実験を行い比較する．ManySAT 手法では求解数の 平均 (小数点以下四捨五入，以下同様) は 526(258+268) で，PAR-2 の平均は 2,479,769 となった．ここで PAR-2 とは各問題の求解時間の合計を示す．ただし求解でき なかった問題に関しては制限時間の 2 倍で解けたと仮 定して合計を算出する．Glucose-Syrup の求解数の平
0 0.2 0.4 0 500 1000 1500 2000 runtime [s] periods 図 3: 既存手法の各 Period での実行時間の分布 均は 537(264+273) であり，PAR-2 の平均は 2,343,707 となった．この結果から ManySAT 手法は，非決定的 並列 SAT ソルバーの Glucose-Syrup と比較すると，求 解数が少なくなり，求解にかかる時間も遅くなってい ることが分かる． もし待ち時間を減らすことができれば，決定的 SAT ソルバーであっても非決定的 SAT ソルバーに匹敵する 性能を持つことができると考えられる．そこで本稿で は待ち時間を低減する手法を提案する．
4
提案手法
4.1
Period の長さの精密化
ManySAT では 1 period の長さ矛盾 700 回と定義し ている．経過時間ではなく矛盾数を使用することで同 期をとるタイミングを決定的にしている．しかし矛盾 700 回にかかる時間は，探索空間や決定変数，学習節 の長さなどの様々な要因によって探索中にも大きく変 化する． 図 3 は，ある問題を既存手法のソルバーで探索した際 の，各 period で 700 回矛盾するまでにかかった実行時 間をソルバーごとに p2000までプロットした図である． もし各ソルバーにおいて period がある一定の実行時間 で動作してくれるならば，ソルバー間の period ごとの 実行時間差がなくなり，待ち時間がなくなるため理想 的である．しかし実際には図 3 のように 1 period にか かる実行時間は一定ではない．このように実行時間が 広く分布する図 3 のようなの場合は，それだけ period ごとの実行時間差が大きく，待ち時間が増加する要因 となる． そこで本手法では矛盾数の代わりに，単位伝播時の 節内のリテラルの走査数 (litscans と表記) を period の長さとする手法を提案する．これは，単位伝搬処理 が SAT ソルバーにおける実行時間の 70∼90%を占め 0 0.2 0 500 1000 1500 2000 runtime [s] periods 図 4: 提案手法の各 Period での実行時間の分布 !" !# $" $# $% $& ' 図 5: マージン手法での学習節交換遅延 ている [3] こと，また学習節の長さが求解中に大きく変 化した場合に矛盾発生にかかる時間は一般的に遅くな るが，リテラルの走査数を基準にすればその影響を無 視できることが理由である． 提案手法によって 1 period にかかる実行時間が一定 に近づいたかどうか，図 3 と同じ手法で検証を行なう． 使用した問題は図 3 と同様である．ここでは 1 period を 2M litscan (M は 106) とした．実験結果を図 4 に示 す．図 3 と比較すると，提案手法はおよそ 0.1 秒付近 に集まっていることがわかる．Period ごとの実行時間 差が小さくなっており，待ち時間の減少が期待できる．4.2
マージン手法
学習節交換を遅延させ待ち時間を減らす手法である マージン手法を提案する．ManySAT 手法では図 1 の ように，piで獲得し export した学習節は，すべてのソ ルバーが piの探索を終えた直後に import していた． それをマージン手法では図 5 のように piで獲得しexport した学習節は，pi+1の探索を終えた直後に
im-port を行なう（マージンが 1 の場合）．このように学 習節の交換を 1 つ遅延させても決定性には影響を与え ない．さらにここで，図 5 の S1の p0について考えて みる．S1の p0は S0よりも早く period を探索したの で，S0が p0の探索を終えるのを待っている．これは学 習節の交換を決定的にするためであったが，今回は p0 の探索終了後に交換する節は存在しない（交換を遅延 させるため）．つまり，S1はここで待とうがそのまま
!" !# $" $# $% $& ' 図 6: マージン手法での待ちがいる例 次の p1に進もうが決定性には影響を与えない．S0も S1が次の period に進んでしまったとしても，S1の p0 の export 節はここでは関係ないので問題はない．つま り，S1が p0の探索終了後，他のソルバーすべてが p0 を探索し終えるのを待つ必要はなく，すぐに次の p1の 探索に進んでしまっても問題はない． しかしすべての待ち時間が無くなるわけではない．図 6 を例に取る．図では節交換を 1 つ遅延させ，待ち時間 をなくして探索を進めており，S1が p2の探索を終え， 1 つ前である S0の p1で export した学習節を import している．しかしこの import の時点で S0ではまだ p1 の探索を行なっている．まだ探索中なので節を export する可能性があり，import するタイミングによっては export した節数が変わり，決定的ではなくなってしま う．S1が p2の探索を終え節を import するためには， S0が p1の探索を終えた後にしなければならない．つ まりここで待ち時間が発生する．S0が p1の探索を終 えた後ならば節を import できるので，S1が p2の探索 後節を import するためには S0が p1 の探索を終える まで待つ必要がある． 具体的なマージン手法の定義を行なう．ソルバー Si の pxでの探索を pixと表記する．学習節交換遅延のマー ジンを m (m≥ 0) とし，m period 分だけ，学習節の 交換を遅延させる．なお m = 0 のとき，学習節交換 の遅延はないため ManySAT と同等の手法となる．あ る時刻においてソルバー Siが pixの探索を終え，ソル バー Sj (i̸= j) が pjy を探索中であるとしよう．この とき x− y < m ならば Sj は pjx−mまでの探索を終え ているので学習節を import する．偽ならばまだ pj x−m の探索を終えていないので終わるまで待つ．pi xの探索 後 import する学習節は pj x−mで export された学習節 となり，x− m < 0 のときは import する節が無いため 何も import しない．
5
評価実験
Period の長さを精密化する手法と，待ち時間を削減 するマージン手法の 2 つの提案手法を，Glucose-Syrup に実装し評価する．比較対象として ManySAT の手法 を Glucose-Syrup に実装したものを既存手法 0.4 0.5 0.6 0.7 0.8 0.9 1 0 100 200 300 400 500 600 700 runtime/realtime instances Previous-method Proposed-method 図 7: 提案手法の実行時間の割合 method) とし，2 つの手法を適用した提案手法 (proposed-method) と評価を行う．パラメータとして，マージン m = 20，1 period の長さとして 2M litscans を用いて 実験を行った．これらのパラメータは予備実験により 決定した．5.1
コア数 4 の評価実験
実験環境は先程と同様である．提案手法により，待 ち時間の割合がどのくらい減ったのか実験を行なった． 結果を図 7 に示す．提案手法では既存手法よりも待ち 時間の割合を大きく減らすことができていることが分 かる．待ち時間の割合が 10%以上の問題は 90 問ほどし かなく，待ち時間の割合が 20%以上の問題に関しては 20 問ほどにまで減らすことができている． 次に求解数と PAR-2 の結果を示す．乱数の seed 値 を 5 つ用意し実験を行い比較を行った．既存手法の ManySAT 手法では求解数の平均は 526(258+268) で， PAR-2 の平均は 2,479,769 であった．一方，提案手法 では求解数の平均は 533(263+270) となり，PAR-2 の 平均は 2,399,907 であった．この結果から提案手法は 求解数，求解速度ともに性能が向上していることが分 かる．非決定的並列ソルバーである Glucose-Syrup を 10 回実行したときの求解数の平均は 537(264+273) で あり，PAR-2 の平均は 2,343,707 である．よって提案 手法は非決定的並列ソルバーである Glucose-Syrup に 肉迫しており，十分実用に耐えうる性能を示している と考えられる．5.2
コア数を増加させたときの評価実験
ここまでは 4 コアで実験を行なってきたが，コア数 を増やしたとき実行時間の割合，求解数，求解時間がど のように変化するのか実験を行った．実験環境は Intel Xeon E5-2620 (2.1GHz) × 2（コア数 6 × 2 = 12），12 85 (43 + 42) 250803 90 (45 + 45) 191422 92 (45 + 47) 184414 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1 0 10 20 30 40 50 60 70 80 90 100 runtime/realtime instances Previous-method-cores=4 Previous-method-cores=8 Previous-method-cores=12 Proposed-method-cores=4 Proposed-method-cores=8 Proposed-method-cores=12 図 8: コア数を増やしたときの実行時間の割合
28GB RAM であり，評価用問題群として SAT Compe-tition, SAT-Race 2014-2016 Application 部門の全 745 問から 100 問を選定し使用した．制限時間は１問あたり 5000 秒とした．提案手法と，Glucose-Syrup 4.1，既存 手法の 3 つを比較する．結果を図 8 に示す．なお cores はコア数を表す．図 8 から，提案手法は，既存手法と 比較して，コア数が増加しても待ち時間の割合の増加 が緩やかになっており，その割合も大幅に削減できて いることが分かる． 次に求解数と PAR-2 の結果を表 1 に示す．表 1 から， 4 コアでは提案手法の求解数は既存手法と同等である ものの，PAR-2 では提案手法が上回っており，求解速 度が速いことが分かる．コア数が 8,12 と増加していっ たときは提案手法と既存手法の差は顕著になり，待ち 時間の削減効果が出ているといえる．さらに非決定的 な Glucose-Syrup と提案手法を比較をしても，遜色な い結果を示しており，コア数が増えても性能が落ちる といった傾向は見られない．提案手法では，Glucose-Syrup と同様に，コア数を更に増加させても性能が伸 びることが期待できるといえる．
6
まとめと今後の課題
本研究では，非決定的並列 SAT ソルバーに近い求解 性能を持つ，決定的並列 SAT ソルバーのための待ち 時間削減手法を提案した．既存の決定的並列 SAT ソル バーの手法を基本に，同期までの間隔の精密化と節交 換を遅延させる 2 つの手法により，決定的並列 SAT ソ ルバーでありながら非決定的並列 SAT ソルバーに肉迫 する求解性能を持つ結果を示し，ソルバーのコア数を 増加させた場合でも性能向上が期待できることを示し た．今後の課題としてさらなるメニーコア環境での評 価実験，提案手法をベースとした並列 SAT ソルバーの ための技術開発などが挙げられる．参考文献
[1] Davis, M., Logemann, G. and Loveland, D.: A Machine Program for Theorem Proving,
Commu-nications of the ACM, Vol. 5, No. 7, pp. 394-397
(1962)
[2] Silva, J. P. M. and Sakallah, K. A.: GRASP : A Search Algorithm for Propositional Satisfiability,
IEEE Transactions on Computers, Vol. 48, pp.
506-521 (1999)
[3] Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L. and Malik, S.: Chaff : Engineering an Efficient SAT Solver, in Proceedings of DAC-01, pp. 530-535 (2001)
[4] Audemard, G. and Simon, L.: Lazy Clause Ex-change Policy for Parallel SAT Solvers, Theory
and Applications of Satisfiability Testing SAT 2014, pp. 197-205 (2014)
[5] Hamadi, Y., Jabbour, S., Piette, C. and Sa¨ıs, L.: Deterministic Parallel DPLL (DP2LL), Journal
