Satisfiability solver The Deduction algorithm Deductionとは • 探索木の先を見る。 • Decisionの変数割り当ての結果を返す事が目的。 • 戻り値は3種類 – SATISFIABLE – CONFLICT – UNKNOWN • UNKNOWNが出る限り、Decisionを繰り返す。 Unit Clause Rule(1) • Deduction mechanismの一つ。 • 最も効率的だと言われている。 • SATのほとんどでこの手法が使われている。 Unit Clause Rule(2) 定義 Clause内のLiteralに関して、1つのLiteralを除く全てのLiteralがFalseの場合、残りのLiteralはTrueと割り当てる事が出来る。具体例 (￢A ∨ B ∨ C ∨ ￢D) 前提：A = True , B = False , C = False 結果：Unit Clause Ruleより、D = Falseとなる。 BCP mechanism • Boolean Constraint Propagation • Decisionの後に、Unit ClauseやConflictを検知するために使う。 • ソルバのデータ構造や振舞いを定義する。 – Counter-Based BCP – Head/Tail List – 2-Literal Watching Counter-Based BCP(1) • 全てのClauseにカウンタを用意する方法。 • 昔は数多くのソルバで適用されていた。 • Counter-Based BCPの一例 – 各Clauseは2つのカウンタを所有する。 • それぞれTrue/FalseなLiteralの数をカウント – 各変数は2つのリストを持っている • それぞれ正/負Literalが出現するClauseを保持 Counter-Based BCP(2) • 変数割り当てがあると、Clauseのカウンタが更新される。 – ClauseのFalseカウンタがLiteralの数と等しくなった場合、CONFLICTである。 – ClauseのFalseカウンタがLiteralの数より1少なくなった場合、Unit Clauseである。 • コストが高い特徴がある – m個のClause 変数がn種類各Clauseが平均l個の Literalを持つ場合、コストはlm/nとなる。 Head/Tail List(1) • 各Clauseは2つのポインタを所有。 – それぞれ、HeadポインタとTailポインタと呼ぶ • Clauseは全てのLiteralを配列で保持する。 – 最初は、HeadポインタはClauseの先頭Literalを、Tailポインタは末尾Literalを指す • 各変数は4つのLinked Listを保持する。それぞれ Head/Tailにポイントされているというフラグを表す。 – – – – Clause_of_pos_head(v) Clause_of_neg_head(v) Clause_of_pos_tail(v) Clause_of_neg_tail(v) Head/Tail List(2) • 例えばClause_of_neg_head(v)は、￢vが Headポインタに指されているClauseを保持するリストである。 Head/Tail List 例題(1) 例えば変数vがTrueを割り当てられた時の事を考えてみよう。まず、矛盾やUnit Clauseを探すには関係のない Clause_of_pos_head(v)と Clause_of_pos_tail(v)は無視される。そのため、neg_head(v)を考えてみる。 neg_head(v)内のClauseに関して探索を行う。 Head/Tail List 例題(2) 探索プロセスにおけるケース 1. 探索を始めて、TrueになってるLiteralを発見した場合、Clauseは充足しているので何もしない。 2. 探索を始めて、最初に自由変数wを見つけた場合、 neg_head(v)よりこのClauseを削除し、head(w)にこの Clauseを追加する。 3. もし2つのポインタ間のLiteralが全てFalseに割り当てられていて、tail Literalが割り当てられていなければ、これはUnit Clauseである。 4. もし2つのポインタ間のLiteralが全てFalseに割り当てられていて、Tail Literalが0に割り当てられていたら、ClauseはCONFLICTである。 Head/Tail List(3) • Head/Tail ListはCounter-Basedよりも速い。 – 例えば変数がTrueと割り当てられた時、 Head/Tailが正LiteralなClauseには訪問しない。 – ポインタ操作のコストはm/nである。(m:Clause の数、n:Literalの種類数) • Counter-BaseとHead/TailはBacktrackに弱い性質を持つ – 変数割当のUndoが複雑 2-Literal Watching(1) • 各Clauseは2つのポインタを所有 – Watching Literal(監視リテラル)と呼ぶ。 • 各変数は2つのリストを所有する。それぞれの変数が出現するClauseを保持する。 – Pos_Watched(v) – Neg_Watched(v) • 実行開始時のポインタ位置はどこでも良い。 • ポインタの移動方向も特に定めない。 2-Literal Watching 例題(1) 変数vがTrueを割り当てられた時の事を考えてみる。Head/Tailと同様、Posのリストは無視する事になる。そこで、Neg(v)に入っているClauseを考える。まず、Clause内の FalseでないLiteral L を探す。この探索中には4つのケースが起きる可能性がある。 2-Literal Watching 例題(2) Negに割当があったケースの分岐 1. もう一方の監視Literalに監視されていないLが存在したら、Neg(v)よりこのClauseを削除し、Lの正/負にそったリストにこのClauseを追加する。この操作をポインタの移動と呼ぶ。 2. もう一方の監視LiteralしかLが存在しなく、さらにLが自由変数ならば、Unit Clauseである。 3. もう一方の監視LiteralしかLが存在しなく、さらにLが Trueな時、何もしなくて良い。 4. もし全てのClauseがFalseに割り当てられ、Lが存在しない場合、CONFLICTである。 2-Literal Watching(2) • Literal Countingフェーズにおいて、Head/Tailと同等の性能を持つ。 • バックトラックにおいて、変数割当のUndoは一定の時間しかかからない。なぜなら2つの監視 LiteralはFalseになった最後のLiteralだからである。 – バックトラック時、監視Literalは共に割当無しになるか、 Trueとなる。 – つまりポインタを移動する必要がない。