DPLLアルゴリズム
DPLLアルゴリズムは、その前身であるデービス・パトナムのアルゴリズムと同様、一階述語論理での定理自動証明で必要だった、命題論理式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。 その効率性のため、現在でも命題論理式の充足可能性問題を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている。
1960年に提案されたデービス・パトナムのアルゴリズムとの違いは、原子論理式除去規則(rule for eliminating atomic formulas)と呼ばれる規則の代わりに、使用メモリの削減のため分割規則と呼ばれる規則を使用することである。通常、この規則はバックトラックを用いて実行される。