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

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

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

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)

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

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

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

The Quest for Efficient Boolean Satisfiability Solvers

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

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

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

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

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

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

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; 　　} 　}

Effective Preprocessing in SAT through Variable and Clause Elimination

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

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 }が残る

(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と呼ぶ。

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と呼ぶ。

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

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

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

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

Benchmark 実行環境 Pave：VT64 Opteron Workstation 4000

Benchmark結果

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

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

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

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

参考文献 [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 : http://www.satcompetition.org/ [4] SatELite , Minisat : http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ [5] zChaff. Boolean Satisfiability Research Group at Princeton: http://www.princeton.edu/~chaff/zchaff.html/ [6] The Satisfiability Library, SAT-03 Competition Problems : http://www.satlib.org/