SATsolver

「SATsolver」の編集履歴（バックアップ）一覧はこちら

「SATsolver」(2005/11/19 (土) 16:59:18) の最新版変更点

追加された行は緑色になります。

削除された行は赤色になります。

<h1>SATsolver</h1>
<hr>
<p><a href=
"http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/The_Deduction_Algorithm.ppt">DeductionAlgorithm（パワポ）</a></p>
<p><a href=
"http://www.ueda.info.waseda.ac.jp/localpage/readings/SAT/cade_cav_2002.pdf">DPLL</a></p>
<p>卒論キックオフ資料　<a href=
"http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/Kickoff/kickoff.pdf">PDF</a>　<a href="http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/Kickoff/kickoff.ppt">PPT</a></p>
<hr>
<p>ネタ･メモをつらつら書いていこう。</p>
<p><strong>意義</strong></p>
<p>
　以下の応用分野に適用できるSATソルバだが、SAT問題はNP完全問題である。何も工夫せずに解こうとすると（総当り）、2のn乗という指数的コストがかかってしまう。要素数がちょっと増えただけで使い物にならなくなってしまうわけだ。SATソルバの大きな目的として、この探索域の削減が挙げられる。調べる必要が無くなった探索域は、ばっさり切り捨ててしまうのだ。</p>
<p>
　SATソルバは長年研究が成されていて、最近はDPLLベースのアルゴリズムに落ち着いているらしい。しかしながら、SATCompetitionという大会があるのだが、そこで1位になるようなSATソルバでも制限時間内に解けない問題が沢山ある。まだまだSAT問題は速く解くことが求められている分野だと言えよう。</p>
<p>
　また、並列環境をうまく利用する事で、SATの性能を何倍にも上げる研究も成されている。並列化において問題になるのは、如何にうまく探索域を分割するかに尽きる。なのだが、SATソルバにおいて探索域は動的であり、大幅に削減される可能性があるため、均等な分割は不可能といえる。</p>
<p>
　SATソルバは2種類ある。『確率的な探索をする事で、素早く充足可能性を見つける。しかし充足不可能性は見出せない』もしくは『虱潰しに探索域を削っていき、最終的に充足可能か充足不可能か判断可能』である。前者は充足可能な問題において力を発揮する。</p>
<p>
　並列環境で考える場合、確率的SATソルバと完全SATソルバを両方の考え方を同時に利用することも可能となる。つまり、PE１で確率的な探索を行い、PE2で完全探索を行い、互いに学習したLemma（後で解説する）を交換すれば、互いの速度向上にも繋がるのではないか。この問題は、充足可能性と比べて充足不可能性の判断が時間かかりそう、って点か。</p>
<h3>メモ</h3>
<p><strong>SATの応用分野</strong></p>
<p>　－AI Planning</p>
<p>
　　　動的制約充足問題や不完全制約充足問題などのバリエーションがある。</p>
<p>　－ハードウェア検証</p>
<p>
　　　LTTLやITLなどで論理式に変換した後に、CNFに直し、SATを解くことで証明する。</p>
<p>　－ソフトウェア検証</p>
<p>　　　上と同じ。</p>
<p>　－定理証明</p>
<p>
　　　SATで証明の検証を行う事が出来る。正当性を示す。</p>
<p><strong>SATの基本用語</strong></p>
<p>　Literal－変数もしくは変数の否定</p>
<p>　Clause－リテラルを論理和（∨）で繋げた物</p>
<p>　Conflict－衝突。まぁ、矛盾の事かね。</p>
<p>
　FreeVariable－自由変数。まだ何も割り当てられてない変数。</p>
<p>
　Desicion－自由変数を分岐ヒューリスティックに従い、真または偽に割り当てる。</p>
<p>
　Implication－Decisionの変数割り当てから決定できる他の自由変数の割り当てを行う。</p>
<p>
　CNF（ConjunctiveNormalForm）－SAT問題ではClauseを論理積（∧）で繋げた形で表現される。CNF表現は探索空間を削減するのに役立つ。</p>
<p>
　バックトラック－衝突が起きたとき、いくつか前のDesicionの状態にClauseを戻す。</p>
<p><strong>DPLLについて</strong></p>
<p>
<strong>　</strong>大まかに言うと、decision→deduce（Implicationみたいなもん）→analyze_conflictの流れで実行される。</p>
<p>　まぁ詳しいアルゴリズムを見ていこうか。</p>
<p>　<strong>Decisionの分岐ヒューリスティック</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　MaximumOccurrencesonMinimumsizedclauses（MOM）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
初期に考案されたヒューリスティック。最小Clauseの中で最も多く出現する自由変数を選ぶ。最も多くのClauseを充足させる･伝播させる事を目標とした貪欲アルゴリズムである。ランダムな問題に強い。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　DynamicLargestCombinedSum（DLIS）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
式全体で最も多く出現する自由変数を選択する。各変数の出現回数を記録するカウンタを使うので実装は簡単なのだが、分岐の効果はとても高い。新たな割り当てやバックトラックが発生した時は、カウンタの値を更新しなければならない。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　VariableStateIndependentDecayingSum（VSIDS）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
LearnClauseを使ったヒューリスティック。変数分のカウンタを用意する。カウンタの初期値は変数の出現個数にする。LearnClauseが加えられた時、その分の変数のカウンタを増やす。そして、カウンタの値は定期的に減少させる。最近アクティブだった変数のカウンタ値が高くなる仕組みだね。VSIDSは良い選択をするにも関わらず、全体実行時間に対する実行時間が少ない。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　Deduceアルゴリズム</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　UnitClauseRule</strong></p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<div class="O" v:shape="_x0000_s2050">
<div style=
"mso-line-spacing: '100 20 0'; mso-margin-left-alt: 216; mso-char-wrap: 1; mso-kinsoku-overflow: 1">
<span lang="EN-US" style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">
Clause</span><span style=
"FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">内の</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">に関して、</span><span style="FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">1</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">つの</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">を除く全ての</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">が</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">False</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">の場合、残りの</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">は</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">True</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">と割り当てる</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">事が出来る。</span></div>
<div style="mso-line-spacing: '100 50 0'; mso-margin-left-alt: 216"></div>
</div>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　BCPメカニズム</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>変数カウンタ方式</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
初期に考案された。各Clauseごとにカウンタを用意し、偽と割り当てられたLiteralをカウント。カウンタがClauseのリテラル数－１になったら、UnitClauseとする。問題がMclause　N変数　LLiteralとすると、新たな変数割り当てがあったときに平均してL*M/N　回の更新が必要となる。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　HeadTailList</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
Clauseの先頭と末尾をポインタによって監視する。また、各変数は4つのリストを所有する。(正/負のHead/TailなClause番号を保持)。Backtrackに弱い。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　2-LiteralWatching</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
Clause中の2つのLiteralをポインタで監視する。ポインタの開始位置はどこでも良い。また、各変数は2つのリストを所有する。詳しくは<a href="http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/The_Deduction_Algorithm.ppt">DeductionAlgorithm（パワポ）</a>を参照。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px"><strong>　Conflict解析</strong></p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px"><font color=
"#330033">CONFLICTが</font>見つかった時、ソルバはdecisionをUndoし、backtrackをする必要がある。ConflictAnalysisは、矛盾の原因を解明し、ソルバを再開させるのを目的とする。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>ChronologicalBacktracking</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
幅優先探索でバックトラックをする。直近のDecisionLevelな変数から順番に、真/偽のどちらか一方を未だ試してない変数が無いか探す。見つけた場合、そこまでバックトラックする。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Antecedent of the Variable</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
UnitClauseによって決定されたClauseのこと。DeductionEngineとしてUnitClauseのみ採用している時に用いられる考え方。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Asserting Clause</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
もしResultClauseのLiteralが全てFalseであるようなら、Assertingと呼ぶ。そしてそのClauseの中で最も最近のDecisionLevelのLiteralが2つ以上重複しない事も条件だ。そして、そのDecisionLevelまでBacktrackする事で、このClauseはUnitClauseとなる。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　<strong>データ構造</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>SparseMatrixRepresentation</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Trie構造</p>
<hr>
<h3 dir="ltr" style="MARGIN-RIGHT: 0px">SAT Competition</h3>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　どんな感じにCNFを表現してるのか。</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　１．まずコード冒頭のにコメント文を書く。これからやる問題の概要とかを書く。（cを冒頭につける）</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　２．次に、これから解く問題のclause数と変数の数を書く。（p　cnf　変数の数　clauseの数）</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　３．そして、CNF文を書いていく。例えば-3　4　2　-10　0　と書いてあったら、￢３∨４∨２∨￢１０の事である。</p>
<h3 dir="ltr" style="MARGIN-RIGHT: 0px">Solver</h3>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　SatELiteGTI</p>
<hr>
<p dir="ltr" style="MARGIN-RIGHT: 0px">Tseitin Transformation</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　参考リンク：<a href=
"http://fmv.jku.at/papers/BiereKunz-ICCAD02.pdf">http://fmv.jku.at/papers/BiereKunz-ICCAD02.pdf</a></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
(x∨￢a∨￢b)∧(￢x∨a)∧(￢x∨b)<br>
⇔　x=a∧b<br>
x→a<br>
x→b<br>
a∧b→x</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">S=(Gx∪Rx)∪(G￢x∪R￢x)<br>
S'=S''∪G'∪R'</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">?</p>
<hr>
<p dir="ltr" style="MARGIN-RIGHT: 0px">SatELiteGTIメモ。</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">./SatELiteGTI +ve+ [benchmark cnf]</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">zChaffがpave用。<br></p>

<h1>SATsolver</h1>
<hr>
<p><a href=
"http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/The_Deduction_Algorithm.ppt">DeductionAlgorithm（パワポ）</a></p>
<p><a href=
"http://www.ueda.info.waseda.ac.jp/localpage/readings/SAT/cade_cav_2002.pdf">DPLL</a></p>
<p>卒論キックオフ資料　<a href=
"http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/Kickoff/kickoff.pdf">PDF</a>　<a href="http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/Kickoff/kickoff.ppt">PPT</a></p>
<hr>
<p>ネタ･メモをつらつら書いていこう。</p>
<p><strong>意義</strong></p>
<p>
　以下の応用分野に適用できるSATソルバだが、SAT問題はNP完全問題である。何も工夫せずに解こうとすると（総当り）、2のn乗という指数的コストがかかってしまう。要素数がちょっと増えただけで使い物にならなくなってしまうわけだ。SATソルバの大きな目的として、この探索域の削減が挙げられる。調べる必要が無くなった探索域は、ばっさり切り捨ててしまうのだ。</p>
<p>
　SATソルバは長年研究が成されていて、最近はDPLLベースのアルゴリズムに落ち着いているらしい。しかしながら、SATCompetitionという大会があるのだが、そこで1位になるようなSATソルバでも制限時間内に解けない問題が沢山ある。まだまだSAT問題は速く解くことが求められている分野だと言えよう。</p>
<p>
　また、並列環境をうまく利用する事で、SATの性能を何倍にも上げる研究も成されている。並列化において問題になるのは、如何にうまく探索域を分割するかに尽きる。なのだが、SATソルバにおいて探索域は動的であり、大幅に削減される可能性があるため、均等な分割は不可能といえる。</p>
<p>
　SATソルバは2種類ある。『確率的な探索をする事で、素早く充足可能性を見つける。しかし充足不可能性は見出せない』もしくは『虱潰しに探索域を削っていき、最終的に充足可能か充足不可能か判断可能』である。前者は充足可能な問題において力を発揮する。</p>
<p>
　並列環境で考える場合、確率的SATソルバと完全SATソルバを両方の考え方を同時に利用することも可能となる。つまり、PE１で確率的な探索を行い、PE2で完全探索を行い、互いに学習したLemma（後で解説する）を交換すれば、互いの速度向上にも繋がるのではないか。この問題は、充足可能性と比べて充足不可能性の判断が時間かかりそう、って点か。</p>
<h3>メモ</h3>
<p><strong>SATの応用分野</strong></p>
<p>　－AI Planning</p>
<p>
　　　動的制約充足問題や不完全制約充足問題などのバリエーションがある。</p>
<p>　－ハードウェア検証</p>
<p>
　　　LTTLやITLなどで論理式に変換した後に、CNFに直し、SATを解くことで証明する。</p>
<p>　－ソフトウェア検証</p>
<p>　　　上と同じ。</p>
<p>　－定理証明</p>
<p>
　　　SATで証明の検証を行う事が出来る。正当性を示す。</p>
<p><strong>SATの基本用語</strong></p>
<p>　Literal－変数もしくは変数の否定</p>
<p>　Clause－リテラルを論理和（∨）で繋げた物</p>
<p>　Conflict－衝突。まぁ、矛盾の事かね。</p>
<p>
　FreeVariable－自由変数。まだ何も割り当てられてない変数。</p>
<p>
　Desicion－自由変数を分岐ヒューリスティックに従い、真または偽に割り当てる。</p>
<p>
　Implication－Decisionの変数割り当てから決定できる他の自由変数の割り当てを行う。</p>
<p>
　CNF（ConjunctiveNormalForm）－SAT問題ではClauseを論理積（∧）で繋げた形で表現される。CNF表現は探索空間を削減するのに役立つ。</p>
<p>
　バックトラック－衝突が起きたとき、いくつか前のDesicionの状態にClauseを戻す。</p>
<p><strong>DPLLについて</strong></p>
<p>
<strong>　</strong>大まかに言うと、decision→deduce（Implicationみたいなもん）→analyze_conflictの流れで実行される。</p>
<p>　まぁ詳しいアルゴリズムを見ていこうか。</p>
<p>　<strong>Decisionの分岐ヒューリスティック</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　MaximumOccurrencesonMinimumsizedclauses（MOM）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
初期に考案されたヒューリスティック。最小Clauseの中で最も多く出現する自由変数を選ぶ。最も多くのClauseを充足させる･伝播させる事を目標とした貪欲アルゴリズムである。ランダムな問題に強い。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　DynamicLargestCombinedSum（DLIS）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
式全体で最も多く出現する自由変数を選択する。各変数の出現回数を記録するカウンタを使うので実装は簡単なのだが、分岐の効果はとても高い。新たな割り当てやバックトラックが発生した時は、カウンタの値を更新しなければならない。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　VariableStateIndependentDecayingSum（VSIDS）</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
LearnClauseを使ったヒューリスティック。変数分のカウンタを用意する。カウンタの初期値は変数の出現個数にする。LearnClauseが加えられた時、その分の変数のカウンタを増やす。そして、カウンタの値は定期的に減少させる。最近アクティブだった変数のカウンタ値が高くなる仕組みだね。VSIDSは良い選択をするにも関わらず、全体実行時間に対する実行時間が少ない。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　Deduceアルゴリズム</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　UnitClauseRule</strong></p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<div class="O" v:shape="_x0000_s2050">
<div style=
"mso-line-spacing: '100 20 0'; mso-margin-left-alt: 216; mso-char-wrap: 1; mso-kinsoku-overflow: 1">
<span lang="EN-US" style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">
Clause</span><span style=
"FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">内の</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">に関して、</span><span style="FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">1</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">つの</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">を除く全ての</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">が</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">False</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">の場合、残りの</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">Literal</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">は</span><span lang="EN-US"
style=
"FONT-SIZE: 117%; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'; mso-fareast-language: JA">True</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">と割り当てる</span><span style="FONT-SIZE: 117%; FONT-FAMILY: 'ＭＳ Ｐゴシック'; mso-fareast-font-family: 'ＭＳ Ｐゴシック'; mso-hansi-font-family: 'Times New Roman'">事が出来る。</span></div>
<div style="mso-line-spacing: '100 50 0'; mso-margin-left-alt: 216"></div>
</div>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　BCPメカニズム</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>変数カウンタ方式</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
初期に考案された。各Clauseごとにカウンタを用意し、偽と割り当てられたLiteralをカウント。カウンタがClauseのリテラル数－１になったら、UnitClauseとする。問題がMclause　N変数　LLiteralとすると、新たな変数割り当てがあったときに平均してL*M/N　回の更新が必要となる。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　HeadTailList</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
Clauseの先頭と末尾をポインタによって監視する。また、各変数は4つのリストを所有する。(正/負のHead/TailなClause番号を保持)。Backtrackに弱い。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　2-LiteralWatching</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
Clause中の2つのLiteralをポインタで監視する。ポインタの開始位置はどこでも良い。また、各変数は2つのリストを所有する。詳しくは<a href="http://www.ueda.info.waseda.ac.jp/~tsukatani/SAT/The_Deduction_Algorithm.ppt">DeductionAlgorithm（パワポ）</a>を参照。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px"><strong>　Conflict解析</strong></p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px"><font color=
"#330033">CONFLICTが</font>見つかった時、ソルバはdecisionをUndoし、backtrackをする必要がある。ConflictAnalysisは、矛盾の原因を解明し、ソルバを再開させるのを目的とする。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>ChronologicalBacktracking</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
幅優先探索でバックトラックをする。直近のDecisionLevelな変数から順番に、真/偽のどちらか一方を未だ試してない変数が無いか探す。見つけた場合、そこまでバックトラックする。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Antecedent of the Variable</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
UnitClauseによって決定されたClauseのこと。DeductionEngineとしてUnitClauseのみ採用している時に用いられる考え方。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Asserting Clause</p>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<p dir="ltr" style="MARGIN-RIGHT: 0px">
もしResultClauseのLiteralが全てFalseであるようなら、Assertingと呼ぶ。そしてそのClauseの中で最も最近のDecisionLevelのLiteralが2つ以上重複しない事も条件だ。そして、そのDecisionLevelまでBacktrackする事で、このClauseはUnitClauseとなる。</p>
</blockquote>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　<strong>データ構造</strong></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
<strong>　　</strong>SparseMatrixRepresentation</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　　Trie構造</p>
<hr>
<h3 dir="ltr" style="MARGIN-RIGHT: 0px">SAT Competition</h3>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　どんな感じにCNFを表現してるのか。</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　１．まずコード冒頭のにコメント文を書く。これからやる問題の概要とかを書く。（cを冒頭につける）</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　２．次に、これから解く問題のclause数と変数の数を書く。（p　cnf　変数の数　clauseの数）</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
　　３．そして、CNF文を書いていく。例えば-3　4　2　-10　0　と書いてあったら、￢３∨４∨２∨￢１０の事である。</p>
<h3 dir="ltr" style="MARGIN-RIGHT: 0px">Solver</h3>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　SatELiteGTI</p>
<hr>
<p dir="ltr" style="MARGIN-RIGHT: 0px">Tseitin Transformation</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">　参考リンク：<a href=
"http://fmv.jku.at/papers/BiereKunz-ICCAD02.pdf">http://fmv.jku.at/papers/BiereKunz-ICCAD02.pdf</a></p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">
(x∨￢a∨￢b)∧(￢x∨a)∧(￢x∨b)<br>
⇔　x=a∧b<br>
x→a<br>
x→b<br>
a∧b→x</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">S=(Gx∪Rx)∪(G￢x∪R￢x)<br>
S'=S''∪G'∪R'</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">?</p>
<hr>
<p dir="ltr" style="MARGIN-RIGHT: 0px">SatELiteGTIメモ。</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">./SatELiteGTI +ve+ [benchmark cnf]</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">zChaffがpave用。<br></p>
<hr>
<p dir="ltr" style="MARGIN-RIGHT: 0px">MPI</p>
<p dir="ltr" style="MARGIN-RIGHT: 0px">printenv　</p>
GXX_ROOT=/usr/lib/gcc-lib/i386-redhat-linux/3.3.2<br>
<p dir="ltr" style="MARGIN-RIGHT: 0px">