Loading article…
論理学およびコンピュータ科学において、デイビス・パトナム・アルゴリズムは、マーティン・デイビスとヒラリー・パトナムによって、命題論理の分解に基づく決定手続きを用いて一階述語論理式の妥当性を検証するために開発されました。有効な一階述語論理式の集合は再帰的に列挙可能ですが再帰的ではないため、この問題を解決する一般的なアルゴリズムは存在しません。したがって、デイビス・パトナム・アルゴリズムは有効な式でのみ終了します。今日では、「デイビス・パトナム・アルゴリズム」という用語は、実際には元のアルゴリズムのステップの1つにすぎない分解に基づく命題論理決定手続き（デイビス・パトナム手続き）と同義語としてよく使われます。
この手順は、充足不能な論理式には充足不能な基本インスタンスが存在することを示唆するヘルブランドの定理と、論理式が有効であるのは、その否定が充足不能である場合に限るという事実に基づいています。これらの事実を総合すると、φの有効性を証明するには、 ¬φの基本インスタンスが充足不能であることを証明すれば十分であることがわかります。φが有効でない場合、充足不能な基本インスタンスの探索は終了しません。
式φの妥当性を検証する手順は、おおよそ以下の3つの部分から構成されます。
最後の部分は、分解に基づくSATソルバー（図に示されているとおり）であり、単位伝播と純粋なリテラル除去（式の中で正または負のみで出現する変数を含む節の除去）を積極的に利用しています。
アルゴリズムDP SAT ソルバー 入力: 節の集合 Φ。 出力：真理値：Φが満たされる場合は真、そうでない場合は偽。
function DP-SAT(Φ) repeat //単位伝播: Φ に単位節 { l }が含まれている間、 l を含むΦ のすべての節cに対して 、Φ ← remove-from-formula ( c , Φ); を 繰り返す。¬ lを含む Φ のすべての節cに対して、 Φ ← remove-from-formula ( c , Φ); を繰り返す。 Φ ← add-to-formula ( c \ {¬ l }, Φ); //正規形ではない節を削除する: Φ 内のリテラルlとその否定 ¬ lの両方を含む節cごとに、 Φ ← remove-from-formula ( c , Φ);を実行する。 //純粋なリテラルの削除: Φ 内のリテラルlがすべて同じ極性を持つ間、l を含むΦ 内のすべての節cに対して 、Φ ← remove-from-formula ( c , Φ); //停止条件: Φ が空の場合はtrue を返す。Φ に空の句が含まれている場合は false を返す。 //デイビス・パトナム手続き: Φ 内のlを含むすべての節cと、その否定 ¬ lを含むすべての節nに対して、 Φ 内の両方の極性で出現する リテラルl を選択する。 // c を n で解決する: r ← ( c \ { l }) ∪ ( n \ {¬ l }); Φ ← add-to-formula ( r , Φ); lまたは ¬ l を含むすべての節cに対して、 Φ ← remove-from-formula ( c , Φ); を 実行します。SATソルバーの各ステップにおいて生成される中間式は、元の式と等充足可能であるが、必ずしも等価ではない。解法ステップでは、最悪の場合、式のサイズが指数関数的に増大する。
デイビス・パトナム・ロゲマン・ラブランドアルゴリズムは、デイビス・パトナム法の命題充足可能性ステップを1962年に改良したもので、最悪の場合でも線形量のメモリしか必要としません。このアルゴリズムは、分割規則の解法を省略しています。つまり、リテラルlを選択し、 lに真の値を代入した簡略化された式が充足可能かどうか、またはlに偽値を代入した簡略化された式が充足可能かどうかを再帰的にチェックするバックトラッキングアルゴリズムです。これは、現在（2015年時点）最も効率的な完全SATソルバーの基礎となっています。