Conflict-Driven-Clause-Learning

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

動作の流れ

分岐（Decision）:

変数に値を仮定し、探索木を構築。

伝播（Propagation）:

仮定した値に基づいて、他の変数の値を決定（ユニットプロパゲーション）。

矛盾の発見（Conflict Detection）:

矛盾が発生した場合、その原因となる節を解析。

学習（Clause Learning）:

矛盾の原因を分析し、新たな節（学習節）を生成。

これにより、同じ矛盾を再び探索しないようにする。

バックトラック（Backtracking）:

矛盾が発生した場所から前に戻り、新たな分岐を試みる。

CDCLでは、単純なバックトラックではなく、矛盾の原因に基づいた「非クロノロジカルバックトラック」を行う。