対立主導の節学習

SAT solving algorithm

コンピュータサイエンスにおいて、衝突駆動型節学習（CDCL ）は、ブール充足可能性問題（SAT）を解くアルゴリズムです。SA​​T問題は、ブール式が与えられた場合、式全体が真となるように変数を割り当てることを求めます。CDCL SATソルバーの内部動作は、DPLLソルバーに着想を得ています。CDCLとDPLLの主な違いは、CDCLのバックジャンプが時系列的ではないことです。^[1]

対立駆動型節学習は、Marques-SilvaとKarem A. Sakallah（1996、1999）^{[2] [3]}およびBayardoとSchrag（1997）^{[4]によって提唱されました。}

背景

ブール充足可能性問題

満足度問題は、連言標準形(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 \lnot A\lor \lnot C}$ ${\displaystyle B\lor C}$

この式を満たす割り当ては、例えば次のようになります。

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

なぜなら、最初の節 (sinceは真) と 2 番目の節 (sinceは真) が真になるからです。 ${\displaystyle \lnot A}$ ${\displaystyle C}$

この例では3つの変数（A、B、C）が使用されており、それぞれに2つの可能な代入（TrueとFalse）があります。つまり、可能性は存在します。この小さな例では、総当たり探索を用いてすべての可能な代入を試し、それらが式を満たすかどうかを確認できます。しかし、数百万もの変数と節を持つ実際のアプリケーションでは、総当たり探索は現実的ではありません。SATソルバーの役割は、複雑なCNF式に対して異なるヒューリスティックを適用することで、効率的かつ迅速に満足のいく代入を見つけることです。 ${\displaystyle 2^{3}=8}$

単位節規則（単位伝播）

ある節のリテラルまたは変数のうち、1つを除いて全てFalseと評価された場合、その節がTrueとなるためには、その自由リテラルがTrueでなければなりません。例えば、以下の不満足な節が で評価された場合、その節がTrueとなる ためにはでなければなりません。 ${\displaystyle A=\mathrm {False} }$ ${\displaystyle B=\mathrm {False} }$ ${\displaystyle C=\mathrm {True} }$ ${\displaystyle (A\lor B\lor C)}$

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

解決

2つの節 と を考えます。2つの節を結合し、 と を削除することで得られる節 は、2つの節の解決子と呼ばれます。 ${\displaystyle (A\lor B\lor C)}$ ${\displaystyle (\neg C\lor D\lor \neg E)}$ ${\displaystyle (A\lor B\lor D\lor \neg E)}$ ${\displaystyle \neg C}$ ${\displaystyle C}$

アルゴリズム

形式化

シーケント計算と同様の記法は、CDCLを含む多くの書き換えアルゴリズムを形式化するために使用できます。以下は、CDCLソルバーが、満足する割り当てが存在しないことを示すために、または満足する割り当てが存在する場合（すなわち、と競合節 ）を見つけるために適用できる規則です。^[6] ${\displaystyle A=(l_{1},\neg l_{2},l_{3},...)}$ ${\displaystyle C}$

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

$${\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{ (Propagate)}}}$$

リテラルが のリテラル集合に含まれ、 も もに含まれない場合、 の真理値を決定し、決定リテラル を拡張します。この規則は、割り当てを強制されない場合は、割り当てる変数を選択し、どの割り当てが選択であったかを記録しておく必要があるという考えを表しています。そうすれば、選択によって満足のいく割り当てが得られなかった場合は、元に戻ることができます。 ${\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{ (Decide)}}}$$

競合 否定がに含まれるような競合節がある場合、競合節を に設定します。このルールは、現在の割り当てにおいて、節内のすべてのリテラルが false に代入されているときに競合を検出することを表します。 ${\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}\}}$

$${\displaystyle {\frac {\begin{array}{c}C={\text{NONE}}\;\;\;\{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{ (Conflict)}}}$$

衝突節がの形式である場合、先行節と がの前に代入されているので、先行節で衝突を解決することで衝突を説明してください。この規則は、現在の衝突節と、衝突節内でリテラルの代入を引き起こした節から暗黙的に導かれる新しい衝突節を導出することで、衝突を説明します。 ${\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{ assigned before }}\neg l\end{array}}{C:=\{l_{1},\dots ,l_{n}\}\cup D}}{\text{ (Explain)}}}$$

バックジャンプ衝突節が という形式である場合、決定レベルにバックジャンプし、 を割り当てて設定します。このルールは、衝突節によって暗黙的に示される決定レベルにジャンプし、より低い決定レベルで衝突を引き起こしたリテラルの否定をアサートすることで、非時系列的なバックトラックを実行します。 ${\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)}}}$$

学習学習済みの節を式に追加できます。このルールはCDCLソルバーの節学習メカニズムを表しており、矛盾する節を節データベースに追加することで、ソルバーが検索ツリーの他の分岐で同じ間違いを繰り返さないようにしています。 ${\displaystyle \Phi }$

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

これら 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{ (Forget)}}}$$

再始動ソルバーは、割り当てを空の割り当てにリセットし、競合節を に設定することで再始動できます。この規則は再始動メカニズムを表しており、ソルバーは潜在的に非生産的な探索空間から抜け出し、学習済みの節に導かれて最初からやり直すことができます。学習済みの節は再始動後も記憶されているため、アルゴリズムの終了が保証されます。 ${\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. 変数を選択し、真偽を割り当てます。これは決定状態と呼ばれます。割り当てを覚えておいてください。
2. ブール制約伝播（単位伝播）を適用します。
3. 含意グラフを構築します。
4. 何らかの矛盾がある場合
   1. 衝突につながった含意グラフのカットを見つける
   2. 衝突の原因となった割り当てを否定する新しい節を導出する
   3. 紛争に関係する最初の変数が割り当てられた適切な決定レベルに、時系列に逆戻り（「バックジャンプ」）する。
5. それ以外の場合は、すべての変数値が割り当てられるまで手順 1 から続行します。

例

CDCLアルゴリズムの視覚的な例: ^[5]

• 
  まず分岐変数x1を選択します。黄色の丸は任意の決定を意味します。
• 
  ここで単位伝播を適用すると、x4は必ず1（つまりTrue）となることがわかります。灰色の円は、単位伝播中に強制的に変数が代入されたことを意味します。結果として得られるグラフは含意グラフと呼ばれます。
• 
  任意に別の分岐変数x3を選択します。
• 
  単位伝播を適用し、新しい含意グラフを見つけます。
• 
  ここで、変数x8とx12はそれぞれ 0 と 1 に強制されます。
• 
  別の分岐変数x2を選択します。
• 
  含意グラフを見つけます。
• 
  別の分岐変数x7を選択します。
• 
  含意グラフを見つけます。
• 
  競合を発見しました!
• 
  この競合の原因となったカットを見つけてください。そのカットから、競合する条件を見つけてください。
• 
  この条件の否定を取って節にします。
• 
  問題に衝突条項を追加します。
• 
  適切な決定レベル（この場合は、学習した節内のリテラルの 2 番目に高い決定レベル）への非時系列バックジャンプ。
• 
  戻ってジャンプし、それに応じて変数値を設定します。

完全

DPLLはSATのための健全かつ完全なアルゴリズムであり、DPLLがϕに対する満足な割り当てを見つけることができる場合のみ、式ϕは満足可能である。CDCL SATソルバーはDPLLを実装しているが、新しい節を学習し、非時系列的にバックトラックすることができる。衝突分析を伴う節学習は健全性にも完全性にも影響を与えない。衝突分析は解決操作を用いて新しい節を識別する。したがって、学習した各節は、一連の解決手順によって元の節および他の学習した節から推論することができる。cNが新しい学習した節である場合、ϕが満足可能であるのは、ϕ ∪ {cN}も満足可能である場合のみである。さらに、バックトラック情報は各新しい学習した節から取得されるため、修正されたバックトラック手順も健全性や完全性に影響を与えない。^[7]

アプリケーション

CDCL アルゴリズムの主な用途は、次のようなさまざまな SAT ソルバーです。

• ミニサット
• ズチャフSAT
• Z3
• グルコース^[8]
• ManySATなど

CDCL アルゴリズムにより、SAT ソルバーは非常に強力になり、 AI 計画、バイオインフォマティクス、ソフトウェア テスト パターン生成、ソフトウェア パッケージの依存関係、ハードウェアおよびソフトウェアモデルのチェック、暗号化など、いくつかの^{[引用が必要]}実際のアプリケーション領域で効果的に使用されています。

関連アルゴリズム

CDCLに関連するアルゴリズムには、デイビス・パトナムアルゴリズムとDPLLアルゴリズムがあります。DPアルゴリズムは導出反駁法を用いており、メモリアクセスの問題が発生する可能性があります。^[要出典] DPLLアルゴリズムはランダムに生成されたインスタンスには適していますが、実用的に生成されるインスタンスには適していません。CDCLは、DPLLと比較 して状態空間の探索が少なくなるため、このような問題を解決するためのより強力なアプローチです。

• 
  DPLL: 学習なし、時系列バックトラッキング。
• 
  CDCL: 対立主導の節学習と非時系列的バックトラッキング。

引用文献

1. 「Conflict Driven Clause Learning (CDCL)」. GeeksforGeeks . 2022年11月16日. 2025年11月29日閲覧。
2. JP Marques-Silva; Karem A. Sakallah (1996年11月). 「GRASP - 満足可能性のための新しい探索アルゴリズム」. IEEE国際コンピュータ支援設計会議 (ICCAD) ダイジェスト. pp.  220– 227. CiteSeerX 10.1.1.49.2075 . doi :10.1109/ICCAD.1996.569607. ISBN  978-0-8186-7597-3。
3. JP Marques-Silva; Karem A. Sakallah (1999年5月). 「GRASP: 命題充足可能性のための探索アルゴリズム」(PDF) . IEEE Transactions on Computers . 48 (5): 506– 521. doi :10.1109/12.769433. 2016年3月4日時点のオリジナル(PDF)からアーカイブ。 2014年11月29日閲覧。
4. Roberto J. Bayardo Jr.; Robert C. Schrag (1997). 「CSPルックバック技法を用いた実世界のSA​​T問題の解決」(PDF) . Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI) . pp.  203– 208.
5. 下の図では、「」は「または」を表すために、乗算は「および」を表すために、接尾辞「」は「いいえ」を表すために使用されています。 ${\displaystyle +}$ ${\displaystyle '}$
6. 「Wayback Machine」（PDF） . mathweb.ucsd.edu . オリジナル（PDF）から2024年5月19日にアーカイブ。 2025年10月2日閲覧。
7. Marques-Silva, Joao; Lynce, Ines; Malik, Sharad (2009年2月). 『満足度ハンドブック』（PDF） . IOS Press. p. 138. ISBN 978-1-60750-376-7。
8. 「グルコースのホームページ」。

参考文献

• マーティン・デイビス、ヒラリー・パトナム (1960). 「数量化理論のための計算手順」J. ACM . 7 (3): 201– 215. doi : 10.1145/321033.321034 . S2CID  31888376.
• マーティン・デイビス、ジョージ・ローゲマン、ドナルド・ラブランド（1962年7月）「定理証明のための機械プログラム」Communications of the ACM . 5 (7): 394– 397. doi :10.1145/368273.368557. hdl : 2027/mdp.39015095248095 . S2CID  15866917.
• Matthew W. Moskewicz、Conor F. Madigan、Ying Zhao、Lintao Zhang、Sharad Malik (2001). 「Chaff：効率的なSATソルバーのエンジニアリング」（PDF） . Proc. 38th Ann. Design Automation Conference (DAC) . pp.  530– 535.
• Lintao Zhang、Conor F. Madigan、Matthew H. Moskewicz、Sharad Malik (2001). 「ブール充足可能性ソルバーにおける効率的な衝突駆動学習」(PDF) . IEEE/ACM国際会議論文集 (ICCAD) . pp.  279– 285.
• プレゼンテーション – 「SATを解く：デイビス・パトナム法からZchaff法、そしてその先へ」 Lintao Zhang氏。（いくつかの写真は彼のプレゼンテーションから引用）

Retrieved from "https://en.wikipedia.org/w/index.php?title=Conflict-driven_clause_learning&oldid=1324710926"