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

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

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

概要

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

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

規則

規則として以下のものがあり、リテラルや充足可能な論理式の削除に用いられる。ここでリテラルとは単一の原子論理式、あるいはその否定を表す。 規則を適用すると論理的な意味は変わるが、充足可能性は変わらない。

• 1リテラル規則（one literal rule, unit rule）

リテラル L 1つだけの節があれば、L を含む節を除去し,他の節の否定リテラル ¬L を消去する。

• 純リテラル規則（pure literal rule, affirmative-nagative rule）

節集合の中に否定と肯定の両方が現われないリテラル（純リテラル） L があれば、L を含む節を除去する。

• 原子論理式除去規則（rule for eliminating atomic formulas）

節集合 F の中に否定と肯定の両方があるリテラル L があれば、そのリテラルを除去する。

さらに以下の規則が追加される場合もある。

• 包含規則（subsumption rule）

ある節 C の全てのリテラルが他の節 D に含まれていれば、それらの節 C を除去する。

• クリーンアップ規則（cleanup rule）

原子論理式 A と ¬A とを含む節を全て除去する。

1リテラル規則と純リテラル規則は特定のリテラルを真と解釈することによって充足可能となる節を除去する。1リテラル規則の適用によりさらに別のリテラルが削除可能になる場合は繰り返し規則を適用する。 包含規則は冗長な節を除去する。クリーンアップ規則はトートロジーを含む節の除去である。

原子論理式除去規則は命題論理での導出規則であり、1リテラル規則と純リテラル規則を適用したのちに使用する。規則は以下の式で表すことができる。上式は前提となる親節、下式はそれらから導かれる導出節（resolvent）を表す。

${\frac {l\vee P,\quad \neg l\vee Q}{P\vee Q}}$

アルゴリズムは、与えられた節の集合に対しこれらの規則を繰り返し適用し、以下の結果が求まれば停止する。

• 節が無くなれば（あるいはトートロジーを含む節のみになれば）、結果は充足可能
• 空節（リテラルを含まない節）が生じれば、結果は充足不能

デービス・パトナムのアルゴリズムについて、以下の定理が成り立つ。

節の集合が充足可能である必要十分条件は、このアルゴリズムを適用した結果が充足可能になることである。

歴史

最初、デービス・パトナムのアルゴリズムはエルブランの定理を用いて一階述語論理式の定理を証明するための方法の一部として用いられた。エルブランの定理での証明をそのまま計算機上で実現したギルモアのアルゴリズムよりは効率的で、ギルモアのアルゴリズムがIBM 704上で21分かかっても結果が出なかった問題を容易に手計算で求めることができた。 だが、基礎例を機械的に作り出しその充足不能性を調べるやり方は、多数の無駄な論理式が生成されるため効率が非常に悪く、ギルモアのアルゴリズムと同様、一階述語論理での複雑な論理式の証明はできなかった。

その後、プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、論理式への適当な代入（単一化）によって充足不能性を調べる方法を提案し 、 デービス・パトナムの枠組みにプラウィツのアイデアを組み合わせたロビンソンの導出原理の提案へのとつながっていく。

デービス・パトナムのアルゴリズム自体もより効率のよいDPLLアルゴリズム（Davis-Putnam-Logemann-Loveland algorithm）に発展し、命題論理式の充足可能性問題を解くためのアルゴリズムとして多くの定理証明システムで使用されている。

例

充足不能な論理式

論理式 $\phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$ の充足可能性を考える。

アルゴリズムは以下の動きになる。

$(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$

リテラル1つだけの節 ($\neg p$) に1リテラル規則を適用する。$\neg p$ を真と見なせば $p$ は偽である。

$(q\vee \neg r)\wedge (\neg q)\wedge (r\vee q)$

1リテラル規則はさらに $\neg q$ にも適用できる。

$(\neg r)\wedge (r)$

この式は矛盾を表し明らかに充足不能である。1リテラル規則を $r$、$\neg r$ いずれに適用しても空節（リテラルを含まない節）が導かれる。真偽値をどのように割り当てても空節は充足可能にはならず、全体の論理式が充足不能であることが証明できる。

同じ論理式を節集合の形で表現すると以下のようになる。空節を □ で表す。

$\{\{p,q,\neg r\},\{\neg q,p\},\{\neg p\},\{r,q\}\}$

(1リテラル規則, p = 偽)

$\{\{q,\neg r\},\{\neg q\},\{r,q\}\}$

(1リテラル規則, q = 偽)

$\{\{\neg r\},\{r\}\}$

(1リテラル規則, r = 真)

$\{\$ □ $\}\$

空節が含まれるため、充足不能であることが証明された。

充足可能な論理式

論理式 $\phi =(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$ を考える。

アルゴリズムは以下の動きになる。

$(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$

リテラル $u$ は肯定でしか現れないため純リテラルである。純リテラル規則を適用する。（u = 真）

$(s\vee t)\wedge (\neg s\vee \neg t)$

1リテラル規則、純リテラル規則とも適用できないため、s について原子論理式除去規則を適用する。

$(t\vee \neg t)$

この式はトートロジーのみを含み、充足可能であることが証明できる。さらにクリーンアップ規則を用いれば節が無くなる。

同じ論理式を節集合の形で表現すると以下のようになる。

$\{\{s,t\},\{\neg s,\neg t\},\{p,u\},\{\neg p,u\}\}$

(純リテラル規則, u = 真)

$\{\{s,t\},\{\neg s,\neg t\}\}$

(原子論理式除去規則, $s$ )

$\{\{t,\neg t\}\}$

(クリーンアップ規則, $t$ )

$\left\{\ \right\}$

節集合が空になったので、充足可能であることが証明された。

関連項目

• エルブランの定理
• DPLLアルゴリズム
• ギルモアのアルゴリズム
• 充足可能性問題
• 定理自動証明
• 導出原理

参考文献

• Davis, Martin; Putnam, Hillary (1960). “A Computing Procedure for Quantification Theory”. Journal of the ACM 7 (3): 201–215. http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034. 
• Davis, Martin; Logemann, George, and Loveland, Donald (1962). “A Machine Program for Theorem Proving”. Communications of the ACM 5 (7): 394–397. http://portal.acm.org/citation.cfm?doid=368273.368557. 
• Davis Martin. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
• Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648.
• R. Dechter; Rish, I. "Directional Resolution: The Davis–Putnam Procedure, Revisited". In J. Doyle and E. Sandewall and P. Torasso (ed.). Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94). Kaufmann. pp. 134–145.
• Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers. http://www.cis.upenn.edu/~jean/gbooks/logic.html