デービス・パトナムのアルゴリズム

デービス・パトナムのアルゴリズム: Davis–Putnam algorithm)は、与えられた論理式の充足可能性を調べるアルゴリズムで、連言標準形で表現された命題論理式を対象とする。アメリカ国家安全保障局の支援を受け、一階述語論理での定理自動証明のための方法としてマーチン・デービス英語版Martin Davis)とヒラリー・パトナムHilary Putnam)により1958年に考案され [1]、一般には1960年に発表された [2]。 その後の改良版であるDPLLアルゴリズムDavis-Putnam-Logemann-Loveland algorithm[3]のベースとなるアルゴリズムである。

なお、古い文献ではDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し[3]、正確には異なる。 1960年に提案されたデービス・パトナムのアルゴリズムが導出を使用するのに対し、1962年に提案されたDPLLアルゴリズムバックトラックを使用する[4]

概要

デービス・パトナムのアルゴリズムは、初期の一階述語論理定理自動証明システムで必要だった命題論理式の充足可能/不能のチェックを効率的に行うために考案されたもので、導出規則を含むいくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省くことができる。

一般に、一階述語論理P の証明可能性(恒真性)は ¬P が充足不能(恒偽)かどうかと同値であり、エルブランの定理より ¬P が充足不能ならば、エルブラン領域の要素を述語論理式に代入した基礎例(エルブラン基底)の命題論理レベルの充足不能チェックにより、有限ステップで証明可能であることが分かっている。 しかしこの方法を定理自動証明に使おうとすると、多量の命題論理式の充足不能性をチェックする必要がある。デービス・パトナムのアルゴリズムはこのような処理を高速に行うことができる。