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&1=EvFerrXe&ei 0CD0Q6AEwAw#v=onepage&q&f=false
在此处输入图像描述

该算法取自《人工智能一种现代方法》一书。我发现它与那些许多函数递归真的很混淆。特别是，该EXTEND()函数做了什么，递归调用背后的目的是DPLL()什么？

4

2 回答 2

25

DPLL本质上是一种回溯算法，这是递归调用背后的主要思想。

该算法在尝试分配时构建解决方案，您有一个部分解决方案，随着您的继续，它可能会被证明成功或不成功。该算法的天才之处在于如何构建部分解决方案。

首先，让我们定义什么是单元子句：

单元子句是一个子句，它恰好具有一个仍未分配的文字，而其他（已分配的）文字 - 都被分配为 false。
此子句的重要性在于，如果当前赋值有效 - 您可以确定未赋值文字中变量的值是什么 - 因为文字必须为真。

例如：如果我们有一个公式：

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

我们已经分配了：

x1=true, x4=true

然后(~x1 \/ ~x4 \/ x5)是一个单元子句，因为您必须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 是如何工作的：

  • 如果我们有一个包含许多变量的公式{x1,...,xn}，您会发现 DPLL 算法将更快地终止（在公式可满足的情况下） ，具体取决于您选择的变量。您还会发现正确选择（显然）更有帮助。
  • 有多种技术可以帮助您做到这一点，称为变量选择启发式。
  • 还需要对公式的表示进行许多优化，以便您可以快速传播决策和饱和子句，特别是“两个观察文字”技术。
  • SAT真正的突破是基于从句学习。每当您“卡住”时，您都会创建一个新子句以添加到您的数据库中，这将阻止您搜索空间的“无用”区域。关于包含学习从句的最佳策略有很多研究：应该包含哪些，何时包含？
  • MiniSat是一款逼真且高度优化的 SAT 求解器。我发现原始 MiniSat 论文在弄清楚如何进行真正优化的 SAT 求解方面确实让我大开眼界。这真的是一本很棒的读物，如果您有兴趣了解更多关于可靠 SAT 求解器的实施的信息，强烈推荐。

因此，从理论上讲，SAT 的核心是一个非常重要的问题（第一个通过 Karp 进行 NP 完全约简，任何复杂性书籍都会介绍的有趣而乏味的构造技术），但在模型检查和软件验证方面也有非常实际的应用。如果您对如何快速解决 NP 完全问题的经典示例感兴趣，请查看工业级 SAT 求解器的实现，这很有趣！

于 2012-09-22T21:12:49.237 回答