DPLLアルゴリズム

Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。
このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（）の改良版として、1962年に、、が発表した
なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。
概要.
DPLLアルゴリズムは、その前身であるデービス・パトナムのアルゴリズムと同様、一階述語論理での定理自動証明で必要だった、命題論理式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。
その効率性のため、現在でも命題論理式の充足可能性問題を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている。
1960年に提案されたデービス・パトナムのアルゴリズムとの違いは、"原子論理式除去規則"（""）と呼ばれる規則の代わりに、使用メモリの削減のため"分割規則"と呼ばれる規則を使用することである。通常、この規則はバックトラックを用いて実行される。
規則.
DPLLアルゴリズムで使われる規則として以下のものがあり、リテラルや充足可能な節の削除に用いられる。ここでリテラルとは単一の原子論理式、あるいはその否定を表す。
さらに以下の規則が追加される場合もある。
1リテラル規則と純リテラル規則は特定のリテラルを真と解釈することによって充足可能となる節を除去する。1リテラル規則の適用によりさらに別のリテラルが削除可能になる場合は繰り返し規則を適用する。
包含規則は冗長な節を除去する。クリーンアップ規則はトートロジーを含む節の除去である。
分割規則は場合分けで、前出の規則を適用しても節が無くならず、充足不能な節も生じない場合にこの規則を適用する。分割規則による節集合の分割は以下のように行う。
分割したそれぞれの節集合について、再帰的に前出の各ルールを適用していく。分割した節集合のいずれかが充足可能ならば節集合は充足可能と見なせる。これは、与えられた節集合を充足可能にするような真偽値の組み合わせの探索、ととらえることができる。
分割規則は、デービス・パトナムのアルゴリズムで使われた原子論理式除去規則の代わりに導入されたものである。原子論理式除去規則は、命題論理での導出規則であり、以下の定義を持つ。
アルゴリズムは、与えられた節の集合に対しこれらの規則が適用できなくなるまで繰り返す。
これらの規則を適用した結果は以下のようになる。
手続き.
再帰呼び出しを用いたDPLLアルゴリズムの疑似コードは以下のように表現できる。
節集合 "F" が入力で、結果は"充足可能"、"充足不能"のいずれかである。
 DPLL(F):
 1リテラル規則、純リテラル規則などを使い F を単純化
 if F is 空:
 return "充足可能"
 if F is 空節を含む:
 return "充足不能"
 原子論理式 "v" を選択
 真理値 "b" を選択 (true or false)
 if DPLL("v" = "b" とした F ) is "充足可能":
 return "充足可能"
 if DPLL("v" = "¬b" とした F) is "充足可能":
 return "充足可能"
 return "充足不能"
実際のプログラムでは、以下の変更が加えられることがある。
歴史.
最初、DPLLアルゴリズムはエルブランの定理を用いて一階述語論理式の定理を証明するための方法の一部として、IBM 704上で利用された。それ以前にデービス・パトナムのアルゴリズムにもとづいたプログラムが作成されたが、原子論理式除去規則の実行に多量のメモリが必要だったため、その代わりに分割規則が使用された。分割した節集合は外部記憶装置（磁気テープ）をスタックとして使用し処理を行った。その結果、当時知られていたギルモアのアルゴリズムより高速で複雑な論理式を処理することが可能だった
今日でも、DPLLアルゴリズムは命題論理式の充足可能性問題を解くための主要なアルゴリズムの1つとして、多くの定理証明システムで使用されている。
例.
充足不能な論理式.
論理式 formula_1 の充足可能性を考える。
アルゴリズムは以下の動きになる。
同じ論理式を節集合の形で表現すると以下のようになる。空節を □ で表す。
充足可能な論理式.
論理式 formula_16 を考える。
アルゴリズムは以下の動きになる。
同じ論理式を節集合の形で表現すると以下のようになる。