9

命題論理で文の充足可能性をチェックするための DPLL アルゴリズムを理解するのに苦労しています。 http://books.google.co.in/books?id=4fyShrIFXg4C&pg=PA250&lpg=PA250&dq=DPLL+アルゴリズム+from+artificial+intelligence+A+modern+approach&source=bl&ots=oOoZsT8KFd&sig=pdmyUsQZZWw76guWY9eFJKyNsH0&hl=en&sa=LEMQOfGUrre1 0CD0Q6AEwAw#v=ワンページ&q&f=false
ここに画像の説明を入力

このアルゴリズムは、Artificial Intelligence A modern approachという本から取られています。これらの多くの関数の再帰と本当に混乱していると思います。具体的には、このEXTEND()関数は何をするのでしょうか? への再帰呼び出しの背後にある目的は何DPLL()ですか?

4

2 に答える 2

25

DPLLは本質的にバックトラッキング アルゴリズムであり、それが再帰呼び出しの背後にある主なアイデアです。

アルゴリズムは、割り当てを試行しながらソリューションを構築しています。進行するにつれて、成功または失敗する可能性のある部分的なソリューションがあります。アルゴリズムの天才は、部分的なソリューションを構築する方法です。

まず、ユニット句とは何かを定義しましょう。

unit 句は、まだ割り当てられていないリテラルを 1 つだけ持つ句であり、他の (割り当てられた) リテラルはすべて false に割り当てられます。
この句の重要性は、現在の割り当てが有効である場合、割り当てられていないリテラルにある変数の値を判断できることです。リテラルは真でなければならないためです。

例: 式がある場合:

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

そして、すでに割り当てています：

x1=true, x4=true

Then(~x1 \/ ~x4 \/ x5)は unit 句ですx5=true。これは、現在の部分代入でこの句を満たすために代入する必要があるためです。

アルゴリズムの基本的な考え方は次のとおりです。

  1. 変数を「推測」する
  2. 最後の割り当てから作成されたすべての単位句を見つけて、必要な値を割り当てます
  3. 変更がなくなるまでステップ 2 を繰り返し再試行します (推移閉包が見つかります)。
  4. 現在の代入がすべての節に対して true を生成できない場合 - 再帰から折り返し、別の代入を再試行します
  5. 可能な場合 - 別の変数を「推測」する (再帰的に呼び出して 1 に戻す)

終了：

  1. 「戻って」「推測」を変更する場所がない（解決策なし）
  2. すべての節が満たされている (解決策があり、アルゴリズムがそれを見つけた)

詳細と例については、これらの講義スライドを参照することもできます。

使用例と重要性:
DPLL は 50 年前のものですが、今でもほとんどの SAT ソルバーの基礎となっています。
SAT ソルバーは、難しい問題を解決するのに非常に役立ちます。たとえば、ソフトウェア検証では、モデルを一連の式と検証する条件として表し、その上で SAT ソルバーを呼び出します。指数関数的な最悪のケース - 平均的なケースでも十分に高速であり、業界で広く使用されています (主にハードウェア コンポーネントの検証用)。

于 2012-09-22T20:59:58.893 に答える
5

DPLL で使用される手法は、複雑性理論の証明で使用される一般的な手法であり、物事への部分的な割り当てを推測し、残りを埋めようとすることに注意してください。DPLL がこのように機能する理由についての参考文献やインスピレーションについては、SAT に関する複雑性理論の資料を読んでみてください (複雑性理論に関する適切な教科書)。

DPLL を「既製品」で使用すると、実際には非常にくだらない解決策につながります。Amit の回答に加えて、現実的な DPLL の仕組みを理解するための実用的な参考文献をいくつか紹介します。

  • 多くの変数を含む数式がある場合、DPLL アルゴリズムは、選択した変数に応じて(数式が{x1,...,xn}満足できる場合) はるかに迅速に終了することがわかります。また、正しく選択すると (明らかに) より役立つことがわかります。
  • これを行うには、変数選択ヒューリスティックと呼ばれる複数の手法があります。
  • また、決定を迅速に伝播し、節を飽和させることができるように、式の表現で行われる多くの最適化があります。特に、「2 つの監視リテラル」手法があります。
  • SATの真のブレークスルーは、節学習に基づいています。「行き詰まった」ときはいつでも、データベースに追加する新しい句を作成します。これにより、スペースの「役に立たない」領域を検索できなくなります。学習した句を含めるための最良の戦略については、多くの研究が行われてきました。
  • MiniSatは、現実的で高度に最適化された SAT ソルバーです。オリジナルの MiniSat の論文は、本当に最適な SAT 解法を行う方法を理解する上で本当に目を見張るものがあることがわかりました。信頼できる SAT ソルバーの実装について詳しく知りたい場合は、ぜひお読みください。

そのため、本質的に、SAT は理論的な観点から非常に重要な問題です (Karp を介した最初の NP 完全還元、複雑な本が紹介する興味深い退屈な構成手法) だけでなく、モデルのチェックとソフトウェアの検証においても非常に実用的なアプリケーションがあります。NP 完全問題を非常に迅速に解決する方法の古典的な例に興味がある場合は、工業用強度の SAT ソルバーの実装を見てください。楽しいです!

于 2012-09-22T21:12:49.237 に答える