DPLLアルゴリズムのソースを表示

'''Davis-Putnam-Logemann-Lovelandアルゴリズム'''（'''DPLLアルゴリズム'''、{{lang-en-short|Davis-Putnam-Logemann-Loveland algorithm}}）とは、[[数理論理学]]および[[計算機科学]]において、[[論理式 (数学)|論理式]]の[[充足可能性問題|充足可能性]]を調べる[[アルゴリズム]]である。[[連言標準形]]で表現された[[命題論理]]式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。

このアルゴリズムは、[[1960年]]に発表された[[デービス・パトナムのアルゴリズム]]（{{lang-en-short|''Davis–Putnam algorithm''}}）の改良版として、[[1962年]]に{{日本語版にない記事リンク|マーチン・デービス|en|Martin Davis}}、{{日本語版にない記事リンク|ジョージ・ロゲマン|en|George Logemann}}、{{日本語版にない記事リンク|ドナルド・ラブランド|en|Donald W. Loveland}}が発表した
<ref name="Davis1962">{{cite journal
| last=Davis
| first=Martin
| coauthors=Logemann, George, and Loveland, Donald
| title=A Machine Program for Theorem Proving
| journal =Communications of the ACM
| volume=5
| issue=7
| pages = 394–397
| date=1962
| url=http://portal.acm.org/citation.cfm?doid=368273.368557}}
</ref>。

なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し<ref name="Davis1962"/>、正確には異なる。

== 概要 ==
DPLLアルゴリズムは、その前身である[[デービス・パトナムのアルゴリズム]]と同様、[[一階述語論理]]での[[定理自動証明]]で必要だった、[[命題論理]]式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。
その効率性のため、現在でも命題論理式の[[充足可能性問題]]を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている<ref name="Umano2010">例えば、馬野洋平, 他. ''基本対象関数に基づく節を持つCNF論理式の充足可能性判定'', [[電子情報通信学会|電子情報通信学会論文誌]]D, Vol.J-93-D, No. 1, pp.1-9, 2010. 参照</ref>。

[[1960年]]に提案されたデービス・パトナムのアルゴリズムとの違いは、''原子論理式除去規則''（''{{lang|en|rule for eliminating atomic formulas}}''）と呼ばれる規則の代わりに、使用メモリの削減のため''分割規則''と呼ばれる規則を使用することである。通常、この規則は[[バックトラック]]を用いて実行される。

== 規則 ==
DPLLアルゴリズムで使われる規則として以下のものがあり、[[リテラル]]や充足可能な節の削除に用いられる。ここでリテラルとは単一の[[原子論理式]]、あるいはその否定を表す。

* 1リテラル規則（''{{lang|en|one literal rule, unit rule}}''）
:リテラル ''L'' 1つだけの節があれば、''L'' を含む節を除去し、他の節の否定リテラル ''¬L'' を消去する。
* 純リテラル規則（''{{lang|en|pure literal rule, affirmative-nagative rule}}''）
:節集合の中に否定と肯定の両方が現れないリテラル（純リテラル） ''L'' があれば、''L'' を含む節を除去する。
* 分割規則（''{{lang|en|splitting rule, rule of case analysis}}''）
:節集合 ''F'' の中に否定と肯定の両方があるリテラル ''L'' があれば、そのリテラルを真偽に解釈してえられる2つの節集合に分割する。

さらに以下の規則が追加される場合もある。
* 包含規則（''{{lang|en|subsumption rule}}''）
:ある節 ''C'' の全てのリテラルが他の節 ''D'' に含まれていれば、それらの節 ''D'' を除去する。
* クリーンアップ規則（''{{lang|en|cleanup rule}}''）
:[[原子論理式]] ''A'' と ''¬A'' とを含む節を全て除去する。

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

分割規則は場合分けで、前出の規則を適用しても節が無くならず、充足不能な節も生じない場合にこの規則を適用する。分割規則による節集合の分割は以下のように行う。
* ''L'' が真：''L'' を含む全ての節を除去し、他の節の ''¬L'' を取り除く。
* ''L'' が偽：''¬L'' を含む全ての節を除去し、他の節の ''L'' を取り除く。
分割したそれぞれの節集合について、再帰的に前出の各ルールを適用していく。分割した節集合のいずれかが充足可能ならば節集合は充足可能と見なせる。これは、与えられた節集合を充足可能にするような真偽値の組み合わせの[[探索]]、ととらえることができる。

分割規則は、[[デービス・パトナムのアルゴリズム]]で使われた原子論理式除去規則の代わりに導入されたものである。原子論理式除去規則は、命題論理での[[導出|導出規則]]であり、以下の定義を持つ。
* 原子論理式除去規則（''{{lang|en|rule for eliminating atomic formulas}}''）
:節集合 ''F'' の中に否定と肯定の両方があるリテラル ''L'' があれば、そのリテラルを除去する。

アルゴリズムは、与えられた節の集合に対しこれらの規則が適用できなくなるまで繰り返す。
これらの規則を適用した結果は以下のようになる。
* 節が無くなれば、結果は充足可能
* 空節（リテラルを含まない節）が生じるか、分割規則で充足可能な値の組み合わせを見つけられなければ、結果は充足不能

== 手続き ==
[[再帰呼び出し]]を用いたDPLLアルゴリズムの疑似コードは以下のように表現できる<ref name="Alekhnovich2001">Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson. [http://www.math.ias.edu/~misha/papers/dpll.ps Exponential lower bounds for the running time of DPLL algorithms]. Journal of Automated Reasoning, Volume35 , Issue1-3 , pp.51-72, 2001.</ref>。
節集合 ''F'' が入力で、結果は"充足可能"、"充足不能"のいずれかである。

 DPLL(F):
  1リテラル規則、純リテラル規則などを使い F を単純化
  '''if''' F '''is''' 空:
      '''return''' "充足可能"
  '''if''' F '''is''' 空節を含む:
      '''return''' "充足不能"
  原子論理式 ''v'' を選択
  真理値 ''b'' を選択 (true or false)
  '''if''' DPLL(''v'' = ''b'' とした F ) '''is''' "充足可能":
      '''return''' "充足可能"
  '''if''' DPLL(''v'' = ''¬b'' とした F) '''is''' "充足可能":
      '''return''' "充足可能"
  '''return''' "充足不能"

実際のプログラムでは、以下の変更が加えられることがある。
* 純リテラル規則は省略されることが多い。チェックのために手間がかかり十分な効果が得にくいため。
* 分割規則を適用する原子論理式 ''v'' と最初にチェックする真理値 ''b'' の選択には、何らかの[[ヒューリスティック]]を用いる。
* 再帰呼び出しを繰り返しに変え、バックトラックは明示的に行う。
:（1レベル以上のバックトラックにより効率化を行える場合がある）
* 手続き内での情報は学習などにより再利用する。

== 歴史 ==
最初、DPLLアルゴリズムは[[エルブランの定理]]を用いて[[一階述語論理]]式の定理を証明するための方法の一部として、[[IBM 704]]上で利用された。それ以前に[[デービス・パトナムのアルゴリズム]]にもとづいたプログラムが作成されたが、原子論理式除去規則の実行に多量のメモリが必要だったため、その代わりに分割規則が使用された。分割した節集合は外部記憶装置（磁気テープ）をスタックとして使用し処理を行った。その結果、当時知られていた[[ギルモアのアルゴリズム]]より高速で複雑な論理式を処理することが可能だった
<ref name="Davis1962"/><ref name="Davis2001">Davis Martin. ''The Early History of Automated Deduction''. in ''Handbook of Automated Reasoning'', ''Volume I'', Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.</ref>。

今日でも、DPLLアルゴリズムは命題論理式の[[充足可能性問題]]を解くための主要なアルゴリズムの1つとして、多くの[[自動定理証明|定理証明]]システムで使用されている<ref name="Umano2010"></ref>。

== 例 ==
=== 充足不能な論理式 ===
論理式 <math>\phi = (p \vee q \vee \neg r) \wedge (\neg q \vee p) \wedge (\neg p) \wedge (r \vee q)</math> の充足可能性を考える。

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

:<math>(p \vee q \vee \neg r) \wedge (\neg q \vee p) \wedge (\neg p) \wedge (r \vee q)</math>
:リテラル1つだけの節 (<math>\neg p</math>) に1リテラル規則を適用する。<math>\neg p</math> を真と見なせば <math>p</math> は偽である。
:<math>(q \vee \neg r) \wedge (\neg q) \wedge (r \vee q)</math>
:1リテラル規則はさらに <math>\neg q</math> にも適用できる。
:<math>(\neg r) \wedge (r)</math>
:この式は[[矛盾]]を表し明らかに充足不能である。1リテラル規則を <math>r</math>、<math>\neg r</math> いずれに適用しても空節（リテラルを含まない節）が導かれる。真偽値をどのように割り当てても空節は充足可能にはならず、全体の論理式が充足不能であることが証明できる。

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

:<math>\{ \{ p, q, \neg r \}, \{ \neg q, p \}, \{ \neg p \}, \{ r, q \} \}</math>
:(1リテラル規則, p = 偽)
:<math>\{ \{ q, \neg r \}, \{ \neg q \}, \{ r, q \} \}</math>
:(1リテラル規則, q = 偽)
:<math>\{ \{ \neg r \}, \{ r \} \}</math>
:(1リテラル規則, r = 真)
:<math>\{ </math> □ <math> \}</math>
:空節が含まれるため、充足不能であることが証明された。

=== 充足可能な論理式 ===
論理式 <math>\phi = (s \vee t) \wedge (\neg s \vee \neg t) \wedge (p \vee u) \wedge (\neg p \vee u)</math> を考える。

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

:<math>(s \vee t) \wedge (\neg s \vee \neg t) \wedge (p \vee u) \wedge (\neg p \vee u)</math>
:リテラル <math>u</math> は肯定でしか現れないため純リテラルである。純リテラル規則を適用する。（u = 真）
:<math>(s \vee t) \wedge (\neg s \vee \neg t)</math>
:1リテラル規則、純リテラル規則とも適用できず単純化できないため、分割規則を適用する。<math>s = </math> 真/偽に分解する。
:<math>\phi_1 = (s \vee t) \wedge (\neg s \vee \neg t) \{ s/true \} = (\neg t)</math> と
:<math>\phi_2 = (s \vee t) \wedge (\neg s \vee \neg t) \{ s/false \} = (t)</math>
:最初に <math>\phi_1</math> を調べると1リテラル規則より t = 偽 の場合に節が無くなり充足可能であることが分かる。これより全体の論理式が充足可能であることが証明できる。（この例では <math>\phi_2</math> も t = 真 の場合に充足可能である。） DPLLアルゴリズムの実行の過程より、この論理式は u = 真, t = s = 真/偽 の場合に充足可能となることが決定できる。

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

:<math>\{ \{ s, t \}, \{ \neg s, \neg t \}, \{ p, u \}, \{ \neg p, u \} \}</math>
:(純リテラル規則, u = 真)
:<math>\{ \{ s, t \}, \{ \neg s, \neg t \} \}</math>
:(分割規則, <math>s = </math> 真/偽)
:<math>\phi_1 = \{\neg t\}</math> と
:<math>\phi_2 = \{t\}</math>
:(1リテラル規則, <math>\phi_1</math>, t = 偽)
:<math>\{ \}</math>
:節集合が空になったので、充足可能であることが証明された。

== 脚注 ==
<references/>

== 参考文献 ==
* {{cite journal
|last=Davis
|first=Martin
| coauthors= Putnam, Hillary
| title=A Computing Procedure for Quantification Theory
| journal =Journal of the ACM
| volume = 7
| issue = 3
| pages = 201–215
| date = 1960
| url = http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=321034}}
*{{cite journal
| last=Davis
| first=Martin
| coauthors=Logemann, George, and Loveland, Donald
| title=A Machine Program for Theorem Proving
| journal =Communications of the ACM
| volume=5
| issue=7
| pages = 394–397
| date=1962
| url=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.

== 関連項目 ==
* [[エルブランの定理]]
* [[デービス・パトナムのアルゴリズム]]
* [[ギルモアのアルゴリズム]]
* [[充足可能性問題]]
* [[定理自動証明]]
* [[導出|導出原理]]

{{デフォルトソート:DPLLあるこりすむ}}
[[Category:アルゴリズム]]
[[Category:数理論理学]]
[[Category:形式手法]]
[[Category:数学に関する記事]]
[[Category:自動定理証明]]