[解決済み] DPLLアルゴリズムはどのように動作しますか？[クローズド］

質問内容

命題論理における文の充足可能性をチェックするDPLLアルゴリズムが理解できなくて困っています。 http://books.google.co.in/books? id=4fyShrIFXg4C&pg=PA250&lpg=PA250&dq=DPLL+algorithm+from+artificial+intelligence+A+modern+approach&source=bl& ots=oOoZsT8KFd&sig=pdmyUsQZZWw76guWY9eFJKyNsH0&hl=en&sa=X&ei=vBFeUOf1EMLrrQeanoG4DQ&ved=0CD0Q6AEwAw#v=onepage&q&f=false

このアルゴリズムは「Artificial Intelligence A modern approach」という本から引用したものです。関数の再帰が多くて、本当に混乱しそうです。特に EXTEND() を再帰的に呼び出す目的は何なのでしょうか？ DPLL() ?

解決方法は？

その DPLL は、基本的に バックトラック・アルゴリズム これが、再帰呼び出しの主なアイデアです。

このアルゴリズムは、割り当てを試しながら解決策を構築していくものです。このアルゴリズムの天才的なところは、いかにして部分解を構築するかということです。

まず 単位節 とは

単位節とは、未割り当てのリテラルを1つだけ持ち、その他の（割り当てられた）リテラルをすべてfalseに割り当てた節である。
この節の重要性は、現在の代入が有効であれば、未代入のリテラルにある変数の値が何であるかを判断できることです - リテラルは真でなければならないからです。

例えば 数式があったとします。

(x1 \/ x2 \/ x3) /\ (~x1 \/ ~x4 \/ x5) /\ ( ~x1 \/ x4)

そして、すでに割り当て済みです。

x1=true, x4=true

次に (~x1 \/ ~x4 \/ x5) は単位節です。 x5=true を満たすために、現在の部分的な代入でこの節を満たす必要があります。

アルゴリズムの基本的な考え方は

1. 変数を推測する。
2. 最後の割り当てから作成されたすべての単位節を検索し、必要な値を割り当てる
3. 変化がなくなるまでステップ2を繰り返し実行（推移的クロージャの発見）
4. 現在の代入ですべての節が真にならない場合 - 再帰からフォールドバックして、別の代入を再試行します。
5. できる場合 - 別の変数を推測する (再帰的に呼び出して 1 に戻る)

終了する。

1. 戻る場所がなく、推測を変更する（解決策なし）
2. すべての条項を満たす（解があり、アルゴリズムがそれを見つけた）。

を見ることもできます。 講演スライド をご覧ください。

使用例と重要性。
DPLLは50年前のものですが、今でもほとんどのSATソルバーの基礎になっています。
SATソルバーは、難しい問題を解くのに非常に便利です。例えば、ソフトウェアの検証では、モデルを数式のセットで表現し、検証したい条件を指定し、それに対してSATソルバーを呼び出します。ワーストケースは指数関数的ですが、アベレージケースは十分に速く、業界で広く使われています（主にハードウェアコンポーネントの検証用）。