卒論キックオフ 2005/7/27 1G02P058-6　塚谷　修平.

Presentation on theme: "卒論キックオフ 2005/7/27 1G02P058-6　塚谷　修平."— Presentation transcript:

1 卒論キックオフ 2005/7/27 1G02P058-6　塚谷　修平

2 発表の流れ SAT問題とは これまで読んだ論文の概要説明 SAT solverに対するベンチマークの結果 これからの事

3 発表の流れ SAT問題とは これまで読んだ論文の概要説明 SAT solverに対するベンチマークの結果 これからの事

4 SAT問題とは 充足可能性問題 SAT問題は基本的に論理積標準形(Conjunctive Normal Form)で表現される
　『与えられた論理式を充足する変数の割り当てが、少なくとも一つ存在するかどうか』 SAT問題は基本的に論理積標準形(Conjunctive Normal Form)で表現される 変数(Variable):TrueもしくはFalseの値をとる Literal:変数もしくは変数の否定を指す 例．￢a , b　など Clause:Literalが論理和で繋がっている形 例．(￢a∨b∨c) CNF:Clauseが論理積で繋がっている形 例．(￢a∨b∨c)∧(d∨￢e)

5 SATの研究意義 NP完全問題 応用分野 指数的コストがかかる 探索域の削減を課題とする 最先端のソルバでも解けない問題が沢山ある
人工知能・検証･定理証明など

6 発表の流れ SAT問題とは これまで読んだ論文の概要説明 SAT solverに対するベンチマークの結果 これからの事

7 読んだ論文 The Quest for Efficient Boolean Satisfiability Solvers
Effective Preprocessing in SAT through Variable and Clause Elimination CNFを小さくするテクニックの紹介

8 The Quest for Efficient Boolean Satisfiability Solvers

9 SATソルバのフレームワーク Boolean SAT問題を解くために、Davis, Putnam, Logemann and LovelandがDPLLという探索アルゴリズムを考案。 命題論理式をCNFに変換して解く SAT問題を幾つかのフェーズにわけて解く １．Preprocess(前処理) ２．Decision(変数選択) ３．Deduction(推論) ４．Conflict-analysis(矛盾の解析) 現在、多くのSATがDPLLに基づいて作られている

10 Preprocessing SAT問題を解き始める前に、出来るだけ問題を簡単な形にしたい。 コストをかけずに探索空間を削減したい
Pure literal rule , recuresive learning, and intverter graphs…

11 Decision(変数選択) Free Variableの中から、値を割り当てる変数を選び出すフェーズ 選択アルゴリズム
MOM：最小Clauseの中で最も多く出現するFVを選択する、貪欲アルゴリズム DLIS：式全体で最も多く出現するFVを選択 VSIDS：矛盾解析による学習機能を利用してFVを選択

12 Deduction(推論) Decisionの結果を判定する Deduction Mechanism BCP mechanism
SATISFIABLE(充足可能)　→solver終了 CONFLICT(矛盾)　→　Conflict_Analysisフェーズへ UNKNOWN　→　Decisionフェーズへ Deduction Mechanism Unit Clause Rule(Boolean Constraint Propagation) Pure Literal Rule BCP mechanism Counter, Head Tail list, 2-Literal Watching

13 Unit Clause Rule 例． 　(a∨b∨￢c∨￢d)というClauseが存在し、仮にa=False , b=False , c=True という割り当てが成されているとする。すると、このClauseがTrueになるためにはdには必ずFalseが割り当てられる。このルールをUnit Clause Ruleと呼ぶ。

14 Conflict-analysis Deductionによって矛盾が検知された場合、Backtrackをする必要がある。
Chronological backtracking 幅優先探索の挙動をする ランダムな問題に成果をあげる可能性 ランダムじゃない問題には効率的でない Non-Chronological backtracking 矛盾が発生した原因を解析 学習機能 再びDecisionもしくはDeductionフェーズに戻る。

15 DPLLコード status = preprocess(); if (status!=UNKNOWN) return status;
　while(1) { 　　decide_next_branch(); 　　while (true) { 　　　status = deduce(); 　　　if (status == CONFLICT) { 　　　　blevel = analyze_conflict(); 　　　　if (blevel == 0) 　　　　　return UNSATISFIABLE; 　　　　else backtrack(blevel); 　　　} 　　　else if (status == SATISFIABLE) 　　　return SATISFIABLE; 　　　else break; 　　} 　}

16 Effective Preprocessing in SAT through Variable and Clause Elimination

17 CNF Minimizer CNFのサイズを削減するSatELite SatELiteにおける4つのテクニック
Variable elimination Subsumption Self-subsumption Definition

18 Variable Elimination 例題1 (CはClauseとする) C1={ x ∨ a1 ∨ … ∨ an }
　C2={ ￢x ∨ b1 ∨ … ∨ bm } 　上記の2つのClauseを伴っているClauseは 　C = { a1 ∨ … ∨ an ∨ b1 ∨ … ∨ bm } 　と置き換えることができる。 　∵仮にxにbool値を入れた場合 　　x=Trueならば、 { b1 ∨ … ∨ bm } が残る 　　x=Falseならば、 { a1 ∨ … ∨ an }が残る

19 (Self-)Subsumption 例題2 C1⊆C2 (C1 subsume C2 )の時、 C2を除去する。
例題3 　 C1 ={ x ∨ a ∨ b } , C2 ={ ￢x ∨ a} 　(C2があと少しでC1をsubsumeしそう) 　この時、xのresolveで 　 C1’={ a ∨ b} 　と変換でき、 C1’ はC1をsubsumeしている。 　このケースの事をSelf-subsumptionと呼ぶ。

20 Definition 論理回路に関するSAT問題 具体例 論理積回路 x=a∧b
Tseitin Transformation 入力に対して回路の出力は特定の形を成す 具体例 　論理積回路 x=a∧b 　{ x ∨ ￢a ∨ ￢b }∧{ ￢x ∨ a }∧{ ￢x ∨ b } 　論理和回路 x=a∨b 　{ ￢x ∨ a ∨ b }∧{ x ∨ ￢a }∧{ x ∨ ￢b } 　このように、xがCNFを回路で表現できる事をxのdefinitionと呼ぶ。

21 SatELiteのまとめ SatELiteの強み 実用例:SatELiteGTI コストが小さい Solverに組み込む事が容易
SatELiteによるPreprocessing SolverにはMiniSATを起用

22 発表の流れ SAT問題とは これまで読んだ論文の概要説明 SAT solverに対するベンチマークの結果 これからの事

23 Benchmark 目的 使用solver SAT solverを使ってみたかった
SatELiteによるCNF Minimizerの効果の確認 SatELiteGTIとMiniSATの速度を比較 速いSolverとして有名なzChaffとの比較 使用solver SatELiteGTI：Minisat+SatELite。 Minisat：SatELiteと開発元が同じ zChaff:速いことで有名なsolver

24 使用Solverの性能 Sat Competition2005より引用

25 Benchmark 実行環境 Pave：VT64 Opteron Workstation 4000

26 Benchmark結果

27 Benchmark結果 ⊿variable：元のvariable数に対するSatELite処理後の相対割合
⊿Clause:意味的にvariableと同じ Sec:SatELite処理にかかった時間

28 Benchmark結果 分かった事 ｚChaffが解くのに時間を要している問題を、SatELiteGTIが容易く解いている事も。
探索時間の長さは、VariableやClauseの数に依存しているわけではない？ しかしSatELiteプロセスによってsolverの性能向上が見られた。 SatELiteプロセスは時間がかからない

29 発表の流れ SAT問題とは これまで読んだ論文の概要説明 SAT solverに対するベンチマークの結果 これからの事

30 これからについて 卒業論文の方向性 夏休み(8月～9月)の方向性 既存のSolverの高速化 SatELiteGTIに関するデータを取る
不得手などの特徴をより詳しく調査する SatELiteGTIのコード解析 ボトルネックとなっている部分はないか

31 参考文献 [1] Lintao Zhang,Sharad Malik: "The Quest for Efficient Boolean Satisfiability Solvers“ [2] Niklas Eaen and Armin Biere: "Effective Preprocessing in SAT through Variable and Clause Elimination“ [3] SAT Competitions : [4] SatELite , Minisat : [5] zChaff. Boolean Satisfiability Research Group at Princeton: [6] The Satisfiability Library, SAT-03 Competition Problems :