高負荷タスクSAT solverのCDCLの補完的軽量アルゴリズム
SATソルバー、特に現代の主力である CDCL（Conflict-Driven Clause Learning：衝突駆動型節学習） の動作は「毎日指摘ばかりして疲れてしまう判定者」に例えられる。
実際に計算資源（リソース）の面でも「もの凄く疲れる（リソースを使いすぎる）処理」を行っています。
「重すぎるので、もっと軽量な方式（アルゴリズム）が必要だ」という問題意識から、現在の計算機科学では、CDCLのパワーが必要な「重い局面」と、もっと軽量に処理できる「軽い局面」を組み合わせるアプローチが主流になっています。
1. なぜCDCL（判定者）はそれほど疲れるのか？
CDCLは、ただ「これはダメ、あれもダメ」と指摘するだけでなく、「なぜダメだったのか（衝突の原因）」をシーケンスを遡って特定し、二度と同じ間違いを繰り返さないように枝を切る（branch and bound)という作業を毎秒何万回も繰り返しています。
- メモリの圧迫： 指摘が増えれば増えるほど「学習節」が膨大になり、判定者の脳内メモリ（キャッシュやRAM）を埋め尽くします。
- 確認コストの増加： ルールが増えると、今度は「新しい割り当てがルールに違反していないか」をチェックするだけで一苦労になります。
つまり、CDCLは「過去の失敗から完璧に学ぶ賢い判定者」ですが、そのぶんエネルギー消費が激しい（リソースを使いすぎる）のです。
2. 実際に使われている「軽量な方式」への切り替え
そのため、現在の実用的なSATソルバーは、CDCLだけに頼るのではなく、「最初はとにかく軽い判定者で回し、どうしてもダメな時だけCDCLの重い処理を出す」というハイブリッドな戦略をとっています。
① BCP（Boolean Constraint Propagation：二元制約伝播）
CDCLの中で、最も頻繁に行われる「超軽量な判定」です。
ある変数が決まったら、「じゃあここも自動的にこうなるよね」と、数独（ナンプレ）を解くように芋づる式に値を確定させていきます。CDCLのような深い分析（学習）はせず、ただルールに従って右から左へ流すだけなので、非常に高速です（Watch Listという技術でさらに軽量化されています）。
② 局所探索法（Local Search / SLS）
「疲れる分析（CDCL）」を一切やめて、「とりあえずランダムに答えを置いてみて、ダメなところをパチパチ裏返して調整する」という判定者です。
- 特徴: メモリをほとんど使わず超軽量です。ただし、どうしても解が見つからないときに「本当に解がない（充足不能）」と証明することはできません。
③ 定期的な「記憶喪失」（Restart & Clause Delete）
疲弊したCDCL判定者を救うため、ソルバーは定期的に以下のようなリフレッシュを行います。
- リスタート: 探索が行き詰まったら、それまでの作業を全部投げ出して、最初から別のルートでやり直します（ただし、学んだ大事なルールだけは持っていく）。
- 節の削除（Clause Garbage Collection）: 増えすぎたルール（学習節）のうち、「最近あんまり使ってないな」という重要度の低いルールをバサバサ切り捨てて、メモリを軽量化します。
3. P完全性やバックプロパゲーションとのつながり
P-completeのバックプロパゲーションを愚直に巻き戻してすべてのバグを特定しようとすると（CDCLのフルパワー）、計算グラフが巨大な場合にシステムがクラッシュするか、途方もない時間がかかります。
そこで、「対話証明（GKRプロトコルなど）」のような軽量な確率的アプローチや、特定の依存関係だけをザックリ切り落とす「プルーニング（枝切り）」を前処理として挟むことで、「判定者（ソルバー）が本格的に疲れる前に対象を小さくしておく」という設計が不可欠になります。