DPLLアルゴリズム
包含規則は冗長な節を除去する。クリーンアップ規則はトートロジーを含む節の除去である。
分割規則は場合分けで、前出の規則を適用しても節が無くならず、充足不能な節も生じない場合にこの規則を適用する。分割規則による節集合の分割は以下のように行う。
L が真:L を含む全ての節を除去し、他の節の ¬L を取り除く。
L が偽:¬L を含む全ての節を除去し、他の節の L を取り除く。
分割したそれぞれの節集合について、再帰的に前出の各ルールを適用していく。分割した節集合のいずれかが充足可能ならば節集合は充足可能と見なせる。これは、与えられた節集合を充足可能にするような真偽値の組み合わせの探索、ととらえることができる。
分割規則は、デービス・パトナムのアルゴリズムで使われた原子論理式除去規則の代わりに導入されたものである。原子論理式除去規則は、命題論理での導出規則であり、以下の定義を持つ。
原子論理式除去規則(rule for eliminating atomic formulas)
節集合 F の中に否定と肯定の両方があるリテラル L があれば、そのリテラルを除去する。
アルゴリズムは、与えられた節の集合に対しこれらの規則が適用できなくなるまで繰り返す。 これらの規則を適用した結果は以下のようになる。
節が無くなれば、結果は充足可能
空節(リテラルを含まない節)が生じるか、分割規則で充足可能な値の組み合わせを見つけられなければ、結果は充足不能