対立主導の節学習

コンピュータ サイエンスにおいて、衝突駆動節学習( CDCL ) は、ブール充足可能性問題(SAT) を解決するためのアルゴリズムです。ブール式が与えられた場合、SAT 問題では、式全体が true と評価されるように変数を割り当てることが求められます。CDCL SAT ソルバーの内部動作は、 DPLL ソルバーにヒントを得ました。CDCL と DPLL の主な違いは、CDCL のバックジャンプが時系列ではないことです。

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

充足可能性問題は、連言標準形(CNF) で与えられた式に対する満足できる割り当てを見つけることです。

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

( ( Aではない )または( Cではない) )   かつ   ( BまたはC )、

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

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

ここで、A 、 B 、 Cはブール変数、、、、およびはリテラル、およびは節です。 ${\displaystyle \lnotA}$${\displaystyle \lnotC}$${\displaystyle B}$${\displaystyle C}$${\displaystyle \lnot A\lor \lnot C}$${\displaystyle B\or C}$

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

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

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

この例では 3 つの変数 ( A、B、C ) が使用され、それぞれに 2 つの割り当て (True と False) が可能です。つまり、可能性はあります。この小さな例では、ブルート フォース検索を使用して、すべての可能な割り当てを試し、それらが式を満たすかどうかを確認できます。ただし、数百万の変数と句を含む実際のアプリケーションでは、ブルート フォース検索は非現実的です。SA​​T ソルバーの役割は、複雑な 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}$

衝突駆動型の節学習は次のように機能します。

1. 変数を選択し、True または False を割り当てます。これは決定状態と呼ばれます。割り当てを覚えておいてください。
2. ブール制約伝播（単位伝播）を適用します。
3. 含意グラフを構築します。
4. 紛争がある場合
   1. 衝突の原因となった含意グラフのカットを見つける
   2. 衝突の原因となった割り当てを否定する新しい節を導出する
   3. 紛争に関係する最初の変数が割り当てられた適切な決定レベルに、時系列に逆戻り（「バックジャンプ」）する。
5. それ以外の場合は、すべての変数値が割り当てられるまで手順 1 から続行します。

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

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

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

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

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

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

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

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

• マーティン・デイビス、ヒラリー・パトナム (1960)。「数量化理論のための計算手順」。J . ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376。
• Martin Davis、George Logemann、Donald Loveland (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 の解き方: Davis-Putnam から Zchaff まで、そしてその先へ」、Lintao Zhang 氏 (いくつかの写真は彼のプレゼンテーションから引用)