DPLL算法是如何工作的？

Question

我对于命题逻辑中的DPLL算法检查句子的可满足性有些困惑。请参考这本书：《人工智能：一种现代方法》，第250页，了解该算法的详细信息。以下是相关链接：
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
下面是一个示例图像： 这个算法来自于《人工智能现代方法》一书。我发现其中的许多函数递归很令人困惑。特别是，EXTEND() 函数是做什么的？递归调用 DPLL() 的目的是什么？

- Ghost

---

FYI @Ghost，我最近写了一篇博客文章，介绍了SAT求解以及如何提高其效率... - Kristopher Micinski

这至少是第三个问题，基本上是从AIMA复制算法并说：“我不理解它，请解释一下。” - Novak

好的，如果我们不理解它们，我们还能做什么呢？此外，他们对自己的算法提供的解释不多。 - Ghost

@Ghost 阅读他们的算法，思考一下，然后询问更详细的问题，以了解您不理解的内容。 - Kristopher Micinski

https://dev59.com/8lbUa4cB1Zd3GeqPAaKj - Ghost

@KristopherMicinski，你的博客文章现在有新的URL吗？ - Jason Hemann

Answer 1

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

该算法在尝试分配时构建解决方案，你有一个可能成功或不成功的部分解决方案。算法的精髓在于如何构建这部分解决方案。

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

单元子句是具有仅有一个未分配文字的子句，而其他已分配的文字均为false的子句。
该子句的重要性在于，如果当前的赋值是有效的，则可以确定未分配文字中变量的值——因为该文字必须为true。

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

(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求解器以验证所需的条件。虽然最坏情况是指数级的，但平均情况足够快，并且在工业界广泛使用（主要用于验证硬件组件）。

- amit

---

“主要用于验证硬件组件”-- 不完全正确。DPLL 是任何 SMT 求解器的基础，这些求解器在静态分析软件中被更多人绝对广泛地使用（按人数计算）而不是在硬件验证中。虽然在硬件行业中使用比软件行业更广泛，但这肯定是真实的！ - Kristopher Micinski

如果我没记错的话，如果x1为false，x4也应该为false吧？因为如果其中一个为true，那么子句已经满足了。 - Tung Nguyen

@MaxB 我不熟悉迭代局部搜索（ILS），但从维基百科文章中我所理解的很少一点是：（1）ILS用于优化问题，而DPLL用于SAT，即决策问题。（2）ILS是关于如何重新启动（如果我理解正确的话），而DPLL是关于如何加快每次尝试的速度。（3）DPLL已经有将近60年的历史了，而维基百科对ILS的参考文献始于1995年，因此如果有的话，ILS可能源自DPLL :) - amit

请更新链接。 - heretoinfinity

Answer 2

我注意到DPLL中使用的技术是复杂性理论证明中常用的技术，其中您需要猜测一些事物的部分赋值，然后尝试填充其余部分。如果想了解DPLL为什么能够奏效的更多参考资料或灵感，您可以阅读任何一本有关复杂性理论的好教材中围绕SAT的复杂性理论材料。

使用“现成”的DPLL实际上会导致相当糟糕的解决方案，但是有一些关键技巧可以使其表现更好！除了Amit的答案外，我还将给出一些实用参考资料，以了解实际情况下DPLL的工作原理：

• 如果我们有一个带有许多变量{x1,...,xn}的公式，你会发现根据你选择的哪个变量，DPLL算法将更快地终止(在公式可满足的情况下)。你还会发现，选择正确是(显然)更有帮助的。
• 有多种技术可以帮助你做到这一点，称为变量选择启发式。
• 还有一些优化可以在公式的表示中进行，以便您可以快速传播决策和饱和子句，特别是“两个观察文字”技术。
• SAT的真正突破基于子句学习。每当你被“卡住”时，你就创建一个新的子句添加到你的数据库中，这将防止你搜索空间中的“无用”区域。已经有很多关于包括学习子句的最佳策略的研究：应该包括哪些，何时包括？
• MiniSat是一个现实和高度优化的SAT求解器。我发现Original MiniSat paper真正揭示了如何进行最优SAT求解的方法。这是一篇非常好的文章，如果你有兴趣了解可靠的SAT求解器的实现，强烈推荐阅读。

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

- Kristopher Micinski