1 DPLLの概要
1.1 背景と位置づけ
1.1.1 SAT問題との関係
DPLLは、命題論理で与えられた論理式が充足可能かどうかを判定する問題（SAT）を解くための古典的アルゴリズム系列である。SATでは、変数に対して真偽を割り当てたときに式全体が真になるか、あるいは不可能であるかを求める。DPLLはこの判定を、割当てを段階的に作りながら矛盾が出るまで探索し、矛盾が出たら直前の分岐へ戻ることで実現する。
1.1.2 命題論理に対する役割
命題論理では、論理演算子を含む式を基礎単位に分解し、計算可能な形へ整理することが多い。DPLLはその中でも、とりわけ節集合としての表現と相性がよく、節が真となるかどうかを逐次確認しながら探索を進める。SATソルバの基本構成要素として広く参照され、より高度な学習型手法へ至る概念的な土台を与える点で重要である。
1.2 基本アイデア
1.2.1 分岐とバックトラック
アルゴリズムの中核は、未割当ての変数を選び、値（真または偽）を仮に割り当てることから始まる。割当てを一歩進めるたびに、式の各節が満たされる可能性がどう変わるかを反映し、矛盾が見つからない限り探索を継続する。矛盾が発生した場合は、直前までに行った決定のうち、矛盾を引き起こした分岐点へ戻り、別の値を試す。これにより探索は分岐木として構造化される。
1.2.2 矛盾検出による枝刈り
単なる全探索では非効率になりやすいが、DPLLは早期に矛盾を検出することで探索の無駄を減らす。具体的には、割当ての進行によっていずれの可能性でも節が真にならない状態が現れたとき、その枝は充足不能として打ち切られる。さらに、割当てによって他の節が自動的に満たされる場合や、ある値を強制する状況も扱い、分岐回数の削減につなげる。
1.3 入力と表現
1.3.1 CNF形式（節集合）
SATに入力される論理式は多くの場合、CNF（Conjunctive Normal Form）すなわち「節の論理積」として扱われる。CNFでは、式は複数の節（クロ―ズ）の連言として表され、各節はリテラルの論理和で表現される。節集合として管理できるため、どの節が既に真になったか、どの節が未確定か、どの節が破壊されたかを判定しやすい。
1.3.2 リテラルと変数の割当て
リテラルは、ある変数またはその否定に対応する。変数への割当ては、真偽のいずれかを与える操作であり、これによりリテラルの真偽が決まる。節はリテラルのいずれかが真であれば満たされ、全てが偽になったときに矛盾（空節に相当する状態）として扱われる。DPLLではこの性質を利用し、割当ての更新に応じて節の状態を再評価する。
2 アルゴリズムの手順
2.1 初期化と前処理
2.1.1 単位節の探索
最初に行われる重要な簡約は単位節の扱いである。単位節とは、含まれるリテラルが1個だけの節であり、この節が真になるにはそのリテラルが真である必要がある。したがって、単位節が存在するなら対応する変数に値を強制的に割り当てられる。強制割当てによって他の節がさらに単位節へ変化することがあるため、単位節の探索と割当ては反復されることが多い。
2.1.2 純粋リテラルの削除
純粋リテラルとは、式中である変数の肯定形か否定形のどちらか一方だけが出現し、他方が出現しない状況を指す。もし変数に対応する一方の極性が出現していなければ、もう一方を任意に選んでも節を満たす方向に支障がない。よって、その極性を採用する値で変数を固定し、節を簡約できることがある。実装では、純粋リテラルの検出コストと節削減効果の釣り合いを考慮して適用の有無を決める場合がある。
2.2 再帰的探索の中核
2.2.1 変数選択の方針
探索の進行では、未割当ての変数からどれを次に決めるかが分岐の起点になる。DPLLは「どの変数を選ぶか」によって探索木の形が大きく変わるため、選択方針は性能に直結する。基本形では任意の変数を選ぶことも可能だが、一般に効率を高めるため、節への影響が大きい変数を優先する指標が用いられる。選択は単純でも正しい判定が可能である。
2.2.2 値の割当てと再帰呼び出し
選ばれた変数に対して、まずある値を仮定して簡約を適用し、その結果が矛盾を含まないかを確認する。矛盾がなければ再帰的に同様の処理を続行する。再帰が失敗（充足不能）に終わった場合、同じ分岐点に戻って反対の値を試す。この二分岐を繰り返すことで、充足可能解の発見または全探索の完了がもたらされる。
2.3 枝刈りの判定規則
2.3.1 矛盾（空節）の検出
矛盾の検出は枝刈りの核心である。割当てが進んである節の全リテラルが偽になったとき、その節は真になり得ない。CNFでは各節が真である必要があるため、この状態は局所的な矛盾として扱われる。実装上は、空節（リテラルを含まない節）の概念に対応する状態として扱われ、これが生じた枝は直ちに終了する。
2.3.2 充足（全節が真）条件
逆に、全ての節が真になった時点では充足条件が満たされる。未割当ての変数が残っていても、既に節集合が満たされているなら、残りの変数の値は任意である。DPLLはこの到達を成功として停止でき、割当ての一貫性から解が構成される。
2.4 終了条件
2.4.1 充足可能判定
充足可能判定は、成功状態に到達したときに行われる。節集合全体が満たされる割当てが構成できた場合、その割当ては充足解であり、探索は終了する。ここで得られる情報は、具体的な変数への値の割当てであり、以降の利用（モデルの生成など）に繋げられる。
2.4.2 充足不能判定
充足不能判定は、探索木における全ての分岐が失敗したときに成立する。各分岐で矛盾が生じるか、さらに分岐を繰り返しても矛盾を避けられないことが示されると、どの割当ても節集合を同時に満たすことはできない。したがって、最終的に「充足不能」が結論となる。
3 性能と実装上の論点
3.1 探索空間の特徴
3.1.1 冗長分岐の発生
DPLLは矛盾検出を行うが、それでも無駄な枝が生まれることがある。例えば、ある割当ての後に到達する矛盾が、別の分岐経路からも同様に再現される場合がある。このとき、探索は同型の状況を何度も繰り返し、計算資源を消費する。分岐戦略や簡約の強さが、この冗長さの度合いを左右する。
3.1.2 最悪計算量の性質
SAT問題は一般にNP完全であり、DPLLも最悪の場合には指数時間に近い振る舞いを示し得る。すなわち、入力の構造によっては非常に多くの分岐を要し、探索木が急速に膨張する。もっとも、実務の多くのSATインスタンスには構造があり、簡約や選択規則が効果を発揮することで平均的には現実的な時間で解ける場合がある。
3.2 改良規則（簡約）
3.2.1 単位伝播の反復
単位節に基づく割当ては、単発で終わらず連鎖することがある。ある変数への固定が進むことで新たな単位節が生まれ、さらに割当てが増える。この波及を単位伝播と呼び、矛盾が起きるか、これ以上単位が生まれない状態に達するまで繰り返すことで、分岐前に決まる情報を増やせる。
3.2.2 純粋リテラル割当ての扱い
純粋リテラルの利用は、式から不要な節や変数を削減する方向に働く。単位伝播ほどは必ずしも強制力が大きくないことがあり、実装では維持すべき更新コストとの兼ね合いで適用が調整されることがある。適切に行えば、探索の深さを浅くし、処理全体の手数を減らす可能性がある。
3.2.3 式の簡約と節削除
簡約では、割当てにより明らかに満たされた節を削除し、逆に満たされない方向へ働くリテラルを削っていく。例えば、ある節がすでに真になると分かれば、それは残りの決定に依存しないため除去できる。これにより評価対象が減り、探索の各段で必要な計算が軽くなる。ただし、簡約を行うための管理コストが増える場合もあるため、手法とデータ構造の設計が重要となる。
3.3 変数選択ヒューリスティクス
3.3.1 単位節に関する指標
単位節が存在する場合、そこに対応する値は強制されるため、選択というより処理優先度の問題になる。単位節の発見や優先度付けは、分岐回数を抑える効果に直結する。実装では、単位伝播を発火させるための待ち行列やフラグを用い、状態更新の順序を制御することが多い。
3.3.2 出現回数ベースの選択
未割当て変数の選択では、節集合への寄与が大きい変数を優先する考え方がある。代表的には、変数が節中にどれだけ頻繁に出現するかを指標にする方法である。出現が多い変数ほど、割当ての影響が大きく、以後の簡約や矛盾検出に早く反映される可能性が高い。
3.3.3 先読みを用いる場合の考え方
先読みは、分岐先の片方を仮定した際にどれほど早く矛盾や強制が起きるかを見積もる考え方である。全てを正確に予測するのは高コストになり得るため、近似的な評価で意思決定を行う。例えば、特定の深さまでだけ探索して見通しを得る、あるいは簡約の増加量を指標化するなど、計算量と効果のバランスが鍵になる。
3.4 データ構造と運用
3.4.1 節の管理
節をどう格納し、更新するかは性能に影響する。典型的には、節ごとのリテラル集合を保持し、割当てに応じて真偽が変化するかを効率よく検出する必要がある。単純な全節走査は実装容易だが、規模が大きいと遅くなるため、変更が起きた節だけを追跡する仕組みが検討される。
3.4.2 代入履歴と巻き戻し
バックトラックでは、どこまでの割当てを有効としていたかを保存し、戻る際に復元する必要がある。代入履歴は分岐点と整合する形で記録され、巻き戻し時には末尾側から無効化する。整合性を保つために、各割当てがどの決定や伝播に由来するかも追跡する設計が望ましい。
3.4.3 効率的な節評価
節が真になる条件、あるいは矛盾に近づく状況を迅速に検出することが重要である。割当ての更新が頻繁に起きるため、毎回の評価を高コストにしない工夫が求められる。評価の対象範囲を狭めたり、節内で変化の影響があるリテラルだけを中心に扱ったりすることで、探索全体の実行時間を抑えられる。
4 ほかの手法との関係
4.1 古典的DPLLと発展版
4.1.1 制約伝播の強化
発展版では、単位伝播を中心にしつつ、より広い形の制約伝播を取り入れて分岐前に状態を前進させる場合がある。これにより、同じ探索深度でもより多くの情報が確定し、探索木が細くなることがある。強化の度合いは計算コストとの関係で選択される。
4.1.2 分岐戦略の改善
分岐戦略は、変数選択や値の優先順位に関する工夫として発展してきた。単位節や高出現変数を優先するなどの基本方針に加え、過去の失敗状況を参照する形で探索の向きを変える考え方も取り入れられる。結果として、同じDPLL枠組みでも実行効率が大きく異なる。
4.2 CDCL（節学習）との比較
4.2.1 学習の必要性
CDCLは、単に分岐して矛盾した枝を捨てるだけでなく、矛盾の原因に関する情報を「学習した節」として保存する。これにより、同様の状況が別の枝で再現されるのを防ぎ、探索の冗長さを削減できる。古典的DPLLにはこの学習機構がないため、同種の失敗を繰り返す可能性が残る。
4.2.2 バックジャンプの概念
CDCLでは、矛盾が起きたときに直前の分岐へ戻るだけでなく、より上の決定点まで一気に戻る仕組み（バックジャンプ）が使われることがある。学習した情報によって、どの決定の組が矛盾を引き起こしたかが明確になり、戻り位置を賢く選べる。DPLLの単純な巻き戻しよりも探索効率が上がりやすい。
4.3 実用SATソルバへの影響
4.3.1 DPLL系エンジンの役割
現代のSATソルバは多様な技術を統合しており、その中でも分岐と伝播、矛盾検出という枠組みは共通基盤として残っている。DPLLはその共通部分を体系化した考え方であり、実装上の判断（簡約の順序、データ構造、評価戦略）において参照され続けている。
4.3.2 SAT実務での位置づけ
実務では、入力の性質に応じて最適な戦略が変わるため、DPLLの考え方だけでなく学習型や強力な簡約を組み合わせるのが一般的である。それでも、DPLLを理解することは、SATソルバの基本動作と性能の背景を掴む上で有益である。特に、なぜバックトラックが効くのか、どの簡約が節を減らし得るのかといった見通しが得られる。
5 具体例と理解の助け
5.1 簡単なCNF例での実行追跡
5.1.1 代入→簡約の流れ
例として、節集合を次のように考える。（変数は x, y とし）
- (x ∨ y)
- (¬x)
- (¬y ∨ x)
初期状態では単位節 (¬x) が存在するため、x を偽に固定する。すると (x ∨ y) は x が偽なので y が真である必要がある候補になる。さらに (¬y ∨ x) では x が偽なので ¬y を真にする必要があり、これは y が偽であることを強制する。ここで矛盾が見つかり、y を真と偽の両方に要求する状態となるため、この割当ての分岐は破綻となる。
5.1.2 矛盾に至る分岐
上の例では、単位節からの強制だけで矛盾が生じたため、分岐（未割当て変数の二分岐）に到達する前に終了する。これはDPLLの枝刈りが、分岐を行う前段でも有効に働き得ることを示している。探索木の観点では、その枝の深さが浅く切られるため、計算量の節約につながる。
5.2 手計算での確認手順
5.2.1 単位節の扱いの練習
手計算の練習としては、まず与えられた節集合から単位節を探し、対応する変数に強制値を与える。次に、その割当てによって各節のリテラルが真になったか、全てが偽になったかを確認する。新たに単位節が生まれたら同じ手順を続ける。これにより、機械的に矛盾や強制の連鎖を追跡できる。
5.2.2 分岐木の作り方
次に、単位伝播で決まらない変数が残っている場合に、その変数を1つ選び真と偽に分けて分岐木を描く。各分岐の子ノードでは、親ノードでの割当てを継承しつつ、追加の仮定を置いた後に再び簡約と矛盾検出を行う。失敗した葉（矛盾が生じた状態）から、戻って別の値の枝を開くことで、探索全体が再現できる。
5.3 よくある誤解
5.3.1 「枝刈り」と「探索の回数」の違い
枝刈りは、探索が不要な枝を早めに終了させる動作を指す。一方で探索の回数は、その結果としてどれだけ多くの分岐や簡約処理が行われたかという量である。枝刈りが行われても、別の理由で同程度の処理が発生すれば回数が減らないこともあり得る。したがって、枝刈りの有無と探索回数の減少は必ずしも一対一ではない。
5.3.2 充足不能の意味の取り違え
充足不能とは、与えられた節集合を同時に真にする割当てが存在しないという意味である。これは「ある分岐で矛盾が起きた」という局所的な失敗とは異なる。DPLLが充足不能と結論するのは、探索木における全ての分岐が失敗し、どの割当ても矛盾を回避できないことが保証されたときである。