Conflict-Driven-Clause-Learning

CDCLは、DPLL法（Davis-Putnam-Logemann-Loveland）を拡張したアルゴリズムです。SAT問題を探索的に解く中で、矛盾（Conflict）が発生すると、その原因を分析し、新たな節（Clause）を学習して次の探索を効率化します。

• CDCLは、SATソルバーの実装において非常に広く使われており、最新のソルバー（例: MiniSAT, Glucose）はこのアルゴリズムを基盤にしています。

動作の流れ

• 分岐（Decision）:
  • 変数に値を仮定し、探索木を構築。
• 伝播（Propagation）:
  • 仮定した値に基づいて、他の変数の値を決定（ユニットプロパゲーション）。
• 矛盾の発見（Conflict Detection）:
  • 矛盾が発生した場合、その原因となる節を解析。
• 学習（Clause Learning）:
  • 矛盾の原因を分析し、新たな節（学習節）を生成。
  • これにより、同じ矛盾を再び探索しないようにする。
• バックトラック（Backtracking）:
  • 矛盾が発生した場所から前に戻り、新たな分岐を試みる。
• CDCLでは、単純なバックトラックではなく、矛盾の原因に基づいた「非クロノロジカルバックトラック」を行う。