対立に基づく節学習

充足可能性問題とは、連言標準形（CNF）で与えられた論理式に対して、充足可能な割り当てを見つけることである。

そのような公式の例は次のとおりです。

（（Aではない ）または（Cではない））かつ（BまたはC）、  

または、一般的な表記法を用いると：^{[ 5 ]}

${\displaystyle (\lnot A\lor \lnot C)\land (B\lor C)}$

ここで、 A、B、Cはブール変数であり、${\displaystyle \lnot A}$、${\displaystyle \lnot C}$、${\displaystyle B}$、 そして${\displaystyle C}$これらはリテラルであり、${\displaystyle \lAではない\lCではない}$そして${\displaystyle B\lor C}$節です。

この公式に適した課題の例は次のとおりです。

${\displaystyle A=\mathrm {False} ,B=\mathrm {False} ,C=\mathrm {True} }$

なぜなら、最初の節を真にするから（${\displaystyle \lnot A}$（ は である）だけでなく、2 番目（ なので）${\displaystyle C}$（これは真実です）。

この例では 3 つの変数 ( A、B、C ) を使用し、それぞれの変数には 2 つの割り当て (True と False) が可能です。したがって、1 つの変数には$2^3=8$可能性は無限大です。この小さな例では、総当たり探索を使って考えられるすべての割り当てを試して、それらが式を満たすかどうかを確認できます。しかし、数百万もの変数と節を含む現実的なアプリケーションでは、総当たり探索は非現実的です。SA​​Tソルバーの役割は、複雑なCNF式に対してさまざまなヒューリスティックを適用することで、効率的かつ迅速に満足のいく割り当てを見つけることです。

節のリテラルまたは変数のうち 1 つを除くすべてが False と評価された場合、節が True となるためには、自由リテラルが True でなければなりません。たとえば、以下の不満足な節が次のように評価された場合${\displaystyle A=\mathrm {False} }$そして${\displaystyle B=\mathrm {False} }$私たちは持っていなければならない${\displaystyle C=\mathrm {True} }$ 条項のために${\displaystyle (A\lor B\lor C)}$本当だ。

単位節ルールの反復適用は、単位伝播またはブール制約伝播（BCP）と呼ばれます。

2つの節を考えてみましょう${\displaystyle (A\lor B\lor C)}$そして${\displaystyle (\neg C\lor D\lor \neg E)}$条項${\displaystyle (A\lor B\lor D\lor \neg E)}$2 つの節を結合し、両方を削除することによって得られる${\displaystyle \neg C}$そして${\displaystyle C}$は、2つの節の解決項と呼ばれます。

解決文は、その前提と等しく充足可能である（つまり、解決文が充足可能であるのは、その両方の前提が充足可能である場合に限る）。

シーケント計算に類似した記法は、CDCL を含む多くの書き換えアルゴリズムを形式化するために使用できます。以下は、CDCL ソルバーが適用できる規則であり、満足のいく割り当てが存在しないことを示すか、または、つまり、満足のいく割り当てが存在しないことを示すか、または、満足のいく割り当てを見つけるために使用できます。${\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}$および抵触条項${\displaystyle C}$[ ^{6 ]​}

伝播する 式内の句が${\displaystyle \Phi }$割り当てられていないリテラルがちょうど 1 つあります${\displaystyle l}$で${\displaystyle A}$節内の他のすべてのリテラルには false が割り当てられています。${\displaystyle A}$、 伸ばす${\displaystyle A}$と${\displaystyle l}$このルールは、現在偽である節に未設定の変数が1つだけ残っている場合、その変数を強制的に設定して節全体を真にするという考え方を表しています。そうしないと、式は満たされません。

$${\displaystyle {\frac {\begin{array}{c}\{l_{1},\dots ,l_{n},l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\;\;\;\;\;l,\neg l\notin A\end{array}}{A:=A\;l}}{\text{ (伝播)}}}$$

文字通りの${\displaystyle l}$はリテラルのセットに含まれています${\displaystyle \Phi }$そしてどちらも${\displaystyle l}$または${\displaystyle \neg l}$は${\displaystyle A}$そして、次の真理値を決定します。${\displaystyle l}$そして拡張する${\displaystyle A}$決定は文字通り${\displaystyle \bullet l}$このルールは、課題を強制的に行う必要がない場合は、割り当てる変数を選択し、どの割り当てが選択によるものだったかをメモしておく必要があるという考え方を表しています。そうすることで、選択の結果、満足のいく割り当てが得られなかった場合に、元に戻ることができます。

$${\displaystyle {\frac {\begin{array}{c}l\in {\text{Lits}}(\Phi )\;\;\;l,\neg l\notin A\end{array}}{A:=A\;\bullet \;l}}{\text{ (決定)}}}$$

矛盾条項がある場合${\displaystyle \{l_{1},\dots ,l_{n}\}\in \Phi }$それらの否定が${\displaystyle \neg l_{1},\dots ,\neg l_{n}}$は${\displaystyle A}$競合条項を設定する${\displaystyle C}$に${\displaystyle \{l_{1},\dots ,l_{n}\}}$このルールは、現在の割り当てにおいて、節内のすべてのリテラルが false に割り当てられている場合に、競合を検出することを表しています。

$${\displaystyle {\frac {\begin{array}{c}C={\text{なし}}\;\;\;\{l_{1},\dots ,l_{n}\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n}\in A\end{array}}{C:=\{l_{1},\dots ,l_{n}\}}}{\text{ (競合)}}}$$

矛盾条項について説明してください${\displaystyle C}$形式は${\displaystyle \{l\}\cup D}$先行節があります${\displaystyle \{l_{1},\dots ,l_{n},\neg l\}\in \Phi }$そして${\displaystyle \neg l_{1},\dots ,\neg l_{n}}$割り当てられる前に${\displaystyle \neg l}$で${\displaystyle A}$そして、紛争を解決することで説明する${\displaystyle C}$先行節との比較。この規則は、現在の競合節と、競合節内でリテラルの割り当てを引き起こした節から暗示される新しい競合節を導出することで、競合を説明します。

$${\displaystyle {\frac {\begin{array}{c}C=\{l\}\cup D\;\;\;\{l_{1},\dots ,l_{n},\neg l\}\in \Phi \;\;\;\neg l_{1},\dots ,\neg l_{n},\neg l\in A\;\;\;\;\;\neg l_{1},\dots ,\neg l_{n}{\text{ 割り当て前に }}\neg l\end{array}}{C:=\{l_{1},\dots ,l_{n}\}\cup D}}{\text{ (説明)}}}$$

バックジャンプ競合条項${\displaystyle C}$形式は${\displaystyle \{l,l_{1},\dots ,l_{n}\}}$どこ$\displaystyle {\text{lev}}(\neg l_{1})\leq \dots \leq {\text{lev}}(\neg l_{n})=i<{\text{lev}}(\neg l)}$そして、決定レベルに戻る${\displaystyle i}$そして割り当てる${\displaystyle M:=M^{[i]}\neg l}$そして設定する${\displaystyle C:={\text{NONE}}}$このルールは、競合条項によって示される決定レベルにジャンプバックし、より低い決定レベルで競合を引き起こしたリテラルの否定を主張することにより、非時系列的なバックトラックを実行します。

$${\displaystyle {\frac {\begin{array}{c}C=\{l,l_{1},\dots ,l_{n}\}\;\;\;{\text{lev}}(\neg l_{1})\leq \dots \leq {\text{lev}}(\neg l_{n})=i<{\text{lev}}(\neg l)\end{array}}{C:={\text{NONE}}\;\;\;A:=A^{[i]}\;\neg l}}{\text{ (Backjump)}}}$$

学習した条項を式に追加できます${\displaystyle \Phi }$このルールは、CDCLソルバーの節学習メカニズムを表しており、競合する節は節データベースに追加され、ソルバーが検索ツリーの他のブランチで同じ間違いを繰り返すのを防ぎます。

$${\displaystyle {\frac {\begin{array}{c}C\neq {\text{NONE}}\;\;\;C\notin \Phi \end{array}}{\Phi$$ :=\Phi \cup \{C\}}}{\text{ (学習)}}}

これらの6つのルールは基本的なCDCLには十分ですが、最新のSATソルバーの実装では、探索空間をより効率的に探索し、SAT問題をより速く解決するために、通常はヒューリスティック制御による追加のルールも追加されます。

学習済みの条項は式から削除できます${\displaystyle \Phi }$メモリを節約するため。このルールは、節忘却メカニズムを表しており、学習した節のうちあまり有用でない節を削除することで、節データベースのサイズを制御します。${\displaystyle \Phi '\models C}$式は${\displaystyle \Phi '}$条項なし${\displaystyle C}$それでも意味する${\displaystyle C}$、 意味${\displaystyle C}$重複表現です。$${\displaystyle {\frac {\begin{array}{c}C={\text{NONE}}\;\;\;\Phi =\Phi '\cup \{C\}\;\;\;\Phi '\models C\end{array}}{\Phi$$ :=\Phi '}}{\text{ (忘れる)}}}

ソルバーを再起動するには、課題をリセットしてください。${\displaystyle A}$空の割り当てへ${\displaystyle A^{[0]}}$そして、競合条項を設定する${\displaystyle C}$に${\displaystyle {\text{NONE}}}$このルールは再起動メカニズムを表しており、ソルバーが潜在的に非生産的な探索空間から抜け出し、学習済みの節に基づいて最初からやり直すことを可能にします。なお、学習済みの節は再起動後も記憶されるため、アルゴリズムの終了が保証されます。

$${\displaystyle {\frac {\begin{array}{c}\end{array}}{A:=A^{[0]}\;\;\;C:={\text{NONE}}}}{\text{ (Restart)}}}$$

対立に基づく節学習は、以下のように機能します。

1. 変数を選択し、TrueまたはFalseを代入します。これは判定状態と呼ばれます。代入した値を覚えておいてください。
2. ブール制約伝播（単位伝播）を適用する。
3. 含意グラフを作成します。
4. 何らかの衝突が生じた場合：
   1. 紛争を引き起こした含意グラフの切断箇所を見つけてください。
   2. 衝突を引き起こした割り当ての否定である新しい節を導き出す
   3. 時系列に逆戻り（「バックジャンプ」）して、紛争に関係する最初の変数が割り当てられた適切な決定レベルに戻る
5. そうでない場合は、すべての変数値が割り当てられるまでステップ1から続行します。