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