DPLLアルゴリズム
Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、英: Davis-Putnam-Logemann-Loveland algorithm）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。
このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（英: Davis–Putnam algorithm）の改良版として、1962年にマーチン・デービス（英語: Martin Davis）、ジョージ・ロゲマン（英語: George Logemann）、ドナルド・ラブランド（英語: Donald W. Loveland）が発表した。
なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。
概要
DPLLアルゴリズムは、その前身であるデービス・パトナムのアルゴリズムと同様、一階述語論理での定理自動証明で必要だった、命題論理式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。
その効率性のため、現在でも命題論理式の充足可能性問題を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている。
1960年に提案されたデービス・パトナムのアルゴリズムとの違いは、原子論理式除去規則（rule for eliminating atomic formulas）と呼ばれる規則の代わりに、使用メモリの削減のため分割規則と呼ばれる規則を使用することである。通常、この規則はバックトラックを用いて実行される。
歴史
最初、DPLLアルゴリズムはエルブランの定理を用いて一階述語論理式の定理を証明するための方法の一部として、IBM 704上で利用された。それ以前にデービス・パトナムのアルゴリズムにもとづいたプログラムが作成されたが、原子論理式除去規則の実行に多量のメモリが必要だったため、その代わりに分割規則が使用された。分割した節集合は外部記憶装置（磁気テープ）をスタックとして使用し処理を行った。その結果、当時知られていたギルモアのアルゴリズムより高速で複雑な論理式を処理することが可能だった。
今日でも、DPLLアルゴリズムは命題論理式の充足可能性問題を解くための主要なアルゴリズムの1つとして、多くの定理証明システムで使用されている。