局所解の求解にかかる実行時間の比較 .1 実験内容

5.2 章の結果より, 抽出した問題からボトルネックとなっていた局所解を求める部分問題を SAT 問題にエンコードした. その際には QMaxSAT が内部で解いている SAT 問題を CNF ファイルとして出力するエンコーダーを実装し用いた. 出力した CNF を 2 つの逐次 SAT ソルバと 5 つの高速な並列 SAT ソルバで求解し実行時間を計測し

た. ⃝¹ QMaxSAT は予備実験で使用したものを再び使用した. 逐次 SAT ソルバとして

QMaxSAT に用いている⃝² Glucose3.0 と⃝³ Glucose3.0 で simplification 行っている

第8章実験内容と結果 28 バージョンを使用した. 並列 SATソルバとして SAT Competition 2014で優秀な成績を収めた,⃝4 Plingeling [16],⃝5 Treengeling [16],⃝6 pmcSAT [14], ⃝7 PeneLoPe [15], ⃝8

Glucose-syrup [13], を使用した. また, Plingeling, Treengeling, pmcSAT, PeneLoPe は SAT Competition のサイト [26] の EDACC からダウンロードしたソースコードに計測用の関数を追加して計測を行った. Glucose-syrup は, Glucose のホームページ [28] からソースコードをタウンロードし使用した. ソルバの SAT competition における成績について以下に示す. 実行時間 30 分でタイムアウトとした.

Plingeling

Application 1位, Hard combinatorial 2位 Tlingeling

Application 3位, Hard combinatorial 1位 PeneLoPe

Application 2位 pmcSAT

Hard combinatorial 3位 glucose-syrup

Application 4位

8.2.2 結果

QMaxSAT, 逐次ソルバ,並列ソルバを解けた問題数, 平均実行時間, QMaxSAT より速く解けた問題数について比較したものを表 8.2.2 に示す. また, 解けた問題数と実行時間について各ソルバを比較した図を図 8.1, 図 8.2,図 8.3に示す.

表8.2 局所解の求解における QMaxSAT と各SAT ソルバの比較

⃝1 ⃝² ⃝³ ⃝⁴ ⃝⁵ ⃝⁶ ⃝⁷ ⃝⁸ 解けた問題数 100 97 99 100 98 90 93 100 速く解けた問題数基準 43 70 78 63 85 43 91 平均の実行時間(s) 235.60 278.72 219.70 114.79 183.51 284.41 373.48 94.04

実行時間の逆比基準 0.85 1.07 2.05 1.28 0.83 0.63 2.51

第8章実験内容と結果 29

8.2.3 考察

まず, 図の見方について説明する. 図においては右下にあるソルバほど性能がいいことを表している. また, 評価の基準として解けた問題数,実行時間の順に優先度が高い.

図 8.1 では, incremental SAT sloving を用いている QMaxSAT で求解した場合の

⃝1 ^と, incremental SAT solving を用いずに Glugose3.0 で求解した場合の⃝² , そして simplification を用いた Glucose3.0 で求解した場合⃝³ ^{を比較している}. ⃝¹^と⃝² ^の比較により, ⃝¹ の方が高速であることがわかり, incremental SAT solvingによって QMaxSAT が高速化されていることが読み取れる. また, ⃝2 ^と⃝³ ^{の比較により}, ⃝3 ^{の方が高速であ}

ることがわかり, Simplification により部分問題における SAT 問題の求解においても高速化されていることが読み取れる. ⃝¹^と⃝³ ^{の比較により}, ⃝¹ の方が高速であることがわかり, Simplification による高速化より, incremental SAT solving の高速化の方が効果があることが読み取れる.

図 8.2 では, incremental SAT sloving を用いている QMaxSAT で求解した場合の⃝¹ と, incremental SAT solving を用いずに並列 SAT ソルバで求解した場合の⃝⁴^〜⃝⁸ ^を比較している. この比較により, ⃝⁵ ⃝⁶⃝⁷ ^{については}, ⃝¹ の方が高性能であることがわかり,

⃝4 ⃝⁸ ^{については}, ⃝¹ より高性能であることがわかる.

図 8.3 では, 全てのソルバについて比較している. ここで, ⃝²⃝⁶⃝⁷ ^{について比較する} と, 逐次である ⃝² ^{が最も速く}, 局所解における求解に際しては, 高速と言われている並列 SAT ソルバであっても逐次SAT ソルバに劣る場合があるということが言える.

そして, 表 8.2.2 より, QMaxSAT に対して, Gluose-syrup は算術平均で 2.51 倍, Plingeling は算術平均で 2.05 倍高速であったと言える. このことから, ボトルネックとなっていた局所解の求解に有用である並列 SAT ソルバが存在するということが言える.

第8章実験内容と結果 30

図8.1 SAT competitionルールでのCactus プロット

図8.2 SAT competitionルールでのCactus プロット

第8章実験内容と結果 31

図8.3 SAT competitionルールでのCactus プロット

第 9 _章

まとめと今後の課題

9.1 まとめ

本研究では, まず予備実験で QMaxSAT において一部の局所解がボトルネックとなっていることを発見した. そして, そのボトルネックを解消するために並列 SAT ソルバを用いた QMaxSAT の実装を試みた結果, incremental SAT solving と simplification を同時に用いることが困難であり, そのトレードオフのために並列 SAT ソルバを局所解の求解に用いることの有用性が自体が自明ではないことが分かった. そのためボトルネックとなる局所解の求解に並列 SAT ソルバを用いることが有用であるかを実験により検証し

た結果, Partial MaxSAT 問題における局所解の求解に対して有用である並列 SAT ソル

バを見つけることができた. 一般的に並列 SATソルバは,逐次 SAT ソルバと比較して高速であるが,本研究で実験した Partial MaxSAT問題をエンコードしたボトルネックとなる部分問題の求解では, 逐次 SAT ソルバと比較してに並列 SAT ソルバであるにも関わらず性能が劣る物もあった. これらのことから, 部分問題として生成された SAT 問題は,

SAT Competiton におけるベンチマーク問題と傾向の異なる SAT 問題であるといえる.

ドキュメント内 Partial MaxSAT (ページ 33-38)