DPLLアルゴリズム
論理式 φ = ( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle \phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)} の充足可能性を考える。
アルゴリズムは以下の動きになる。
( p ∨ q ∨ ¬ r ) ∧ ( ¬ q ∨ p ) ∧ ( ¬ p ) ∧ ( r ∨ q ) {\displaystyle (p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)}
リテラル1つだけの節 ( ¬ p {\displaystyle \neg p} ) に1リテラル規則を適用する。 ¬ p {\displaystyle \neg p} を真と見なせば p {\displaystyle p} は偽である。
( q ∨ ¬ r ) ∧ ( ¬ q ) ∧ ( r ∨ q ) {\displaystyle (q\vee \neg r)\wedge (\neg q)\wedge (r\vee q)}
1リテラル規則はさらに ¬ q {\displaystyle \neg q} にも適用できる。
( ¬ r ) ∧ ( r ) {\displaystyle (\neg r)\wedge (r)}
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アルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。