DPLLアルゴリズム

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アルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。

概要

DPLLアルゴリズムは、その前身であるデービス・パトナムのアルゴリズムと同様、一階述語論理での定理自動証明で必要だった、命題論理式の充足可能/不能のチェックを効率的に行うために考案されたアルゴリズムである。いくつかの規則を用いることで充足可能であることが分かっている論理式を効率的に削除し、無駄な判定を省いている。 その効率性のため、現在でも命題論理式の充足可能性問題を扱う多くのツールでDPLLアルゴリズムは基本アルゴリズムとして用いられている。

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

規則

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

●1リテラル規則︵one literal rule, unit rule︶

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

●純リテラル規則︵pure literal rule, affirmative-nagative rule︶

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

●分割規則︵splitting rule, rule of case analysis︶

節集合 Fの中に否定と肯定の両方があるリテラル Lがあれば、そのリテラルを真偽に解釈してえられる2つの節集合に分割する。

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

●包含規則︵subsumption rule︶

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

●クリーンアップ規則︵cleanup rule︶

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

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

分割規則は場合分けで、前出の規則を適用しても節が無くならず、充足不能な節も生じない場合にこの規則を適用する。分割規則による節集合の分割は以下のように行う。

●L が真‥L を含む全ての節を除去し、他の節の ¬L を取り除く。

●L が偽‥¬L を含む全ての節を除去し、他の節の Lを取り除く。

分割したそれぞれの節集合について、再帰的に前出の各ルールを適用していく。分割した節集合のいずれかが充足可能ならば節集合は充足可能と見なせる。これは、与えられた節集合を充足可能にするような真偽値の組み合わせの探索、ととらえることができる。

分割規則は、デービス・パトナムのアルゴリズムで使われた原子論理式除去規則の代わりに導入されたものである。原子論理式除去規則は、命題論理での導出規則であり、以下の定義を持つ。

●原子論理式除去規則︵rule for eliminating atomic formulas︶

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

アルゴリズムは、与えられた節の集合に対しこれらの規則が適用できなくなるまで繰り返す。 これらの規則を適用した結果は以下のようになる。

●節が無くなれば、結果は充足可能

●空節︵リテラルを含まない節︶が生じるか、分割規則で充足可能な値の組み合わせを見つけられなければ、結果は充足不能

手続き

再帰呼び出しを用いたDPLLアルゴリズムの疑似コードは以下のように表現できる。 節集合 Fが入力で、結果は"充足可能"、"充足不能"のいずれかである。

DPLL(F):
 1リテラル規則、純リテラル規則などを使いFを単純化
 ifFis 空:
     return "充足可能"
 ifFis 空節を含む:
     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上で利用された。それ以前にデービス・パトナムのアルゴリズムにもとづいたプログラムが作成されたが、原子論理式除去規則の実行に多量のメモリが必要だったため、その代わりに分割規則が使用された。分割した節集合は外部記憶装置︵磁気テープ︶をスタックとして使用し処理を行った。その結果、当時知られていたギルモアのアルゴリズムより高速で複雑な論理式を処理することが可能だった 。

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

例

充足不能な論理式

論理式 $\phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$$\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)$$(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$
リテラル1つだけの節 ($\neg p$$\neg p$) に1リテラル規則を適用する。$\neg p$$\neg p$ を真と見なせば $p$$p$は偽である。

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

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

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

$\{\{p,q,\neg r\},\{\neg q,p\},\{\neg p\},\{r,q\}\}$$\{\{p,q,\neg r\},\{\neg q,p\},\{\neg p\},\{r,q\}\}$
(1リテラル規則, p = 偽)

$\{\{q,\neg r\},\{\neg q\},\{r,q\}\}$$\{\{q,\neg r\},\{\neg q\},\{r,q\}\}$
(1リテラル規則, q = 偽)

$\{\{\neg r\},\{r\}\}$$\{\{\neg r\},\{r\}\}$
(1リテラル規則, r = 真)

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

充足可能な論理式

論理式 $\phi =(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$$\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)$$(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$
リテラル $u$$u$は肯定でしか現れないため純リテラルである。純リテラル規則を適用する。︵u = 真︶

$(s\vee t)\wedge (\neg s\vee \neg t)$$(s\vee t)\wedge (\neg s\vee \neg t)$
1リテラル規則、純リテラル規則とも適用できず単純化できないため、分割規則を適用する。$s=$$s=$ 真/偽に分解する。

$\phi _{1}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/true\}=(\neg t)$$\phi _{1}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/true\}=(\neg t)$ と

${\displaystyle \phi _{2}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/false\}=($t)} $\phi _{2}=(s\vee t)\wedge (\neg s\vee \neg t)\{s/false\}=(t)$
最初に $\phi _{1}$$\phi _{1}$を調べると1リテラル規則より t = 偽 の場合に節が無くなり充足可能であることが分かる。これより全体の論理式が充足可能であることが証明できる。︵この例では $\phi _{2}$$\phi _{2}$も t = 真 の場合に充足可能である。︶ DPLLアルゴリズムの実行の過程より、この論理式は u = 真, t = s = 真/偽 の場合に充足可能となることが決定できる。

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

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

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

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

(分割規則, $s=$ 真/偽)

$\phi _{1}=\{\neg t\}$ と

$\phi _{2}=\{t\}$

(1リテラル規則, $\phi _{1}$, t = 偽)

$\{\}$

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

参考文献

• 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.

関連項目

• エルブランの定理
• デービス・パトナムのアルゴリズム
• ギルモアのアルゴリズム
• 充足可能性問題
• 定理自動証明
• 導出原理