DPLLアルゴリズム
s = {\displaystyle s=} 真/偽に分解する。
φ 1 = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) { s / t r u e } = ( ¬ t ) {\displaystyle \phi _{1}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/true\}=(\neg t)} と
φ 2 = ( s ∨ t ) ∧ ( ¬ s ∨ ¬ t ) { s / f a l s e } = ( t ) {\displaystyle \phi _{2}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/false\}=(t)}
最初に φ 1 {\displaystyle \phi _{1}} を調べると1リテラル規則より t = 偽 の場合に節が無くなり充足可能であることが分かる。これより全体の論理式が充足可能であることが証明できる。(この例では φ 2 {\displaystyle \phi _{2}} も t = 真 の場合に充足可能である。) DPLLアルゴリズムの実行の過程より、この論理式は u = 真, t = s = 真/偽 の場合に充足可能となることが決定できる。
DPLLアルゴリズムで使われる規則として以下のものがあり、リテラルや充足可能な節の削除に用いられる。ここでリテラルとは単一の原子論理式、あるいはその否定を表す。
1リテラル規則(one literal rule, unit rule)
リテラル L 1つだけの節があれば、L を含む節を除去し、他の節の否定リテラル ¬L を消去する。
純リテラル規則(pure literal rule, affirmative-nagative rule)
節集合の中に否定と肯定の両方が現れないリテラル(純リテラル) L があれば、L を含む節を除去する。
分割規則(splitting rule, rule of case analysis)
節集合 F の中に否定と肯定の両方があるリテラル L があれば、そのリテラルを真偽に解釈してえられる2つの節集合に分割する。
さらに以下の規則が追加される場合もある。
包含規則(subsumption rule)
ある節 C の全てのリテラルが他の節 D に含まれていれば、それらの節 D を除去する。
クリーンアップ規則(cleanup rule)
原子論理式 A と ¬A とを含む節を全て除去する。
1リテラル規則と純リテラル規則は特定のリテラルを真と解釈することによって充足可能となる節を除去する。1リテラル規則の適用によりさらに別のリテラルが削除可能になる場合は繰り返し規則を適用する。