DPLL 算法是如何工作的？ [关闭]答案

【问题标题】：How does the DPLL algorithm work? [closed]DPLL 算法是如何工作的？ [关闭]
【发布时间】：2012-09-14 20:35:24
【问题描述】：

我无法理解用于检查命题逻辑中句子可满足性的 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

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

【问题讨论】：

仅供参考@Ghost，我最近写了a blog post，描述了SAT求解，以及如何提高它的效率......
这至少是第三个问题，基本上是从 AIMA 复制一个算法并说，“我不明白，给我解释一下。”
如果我们不理解他们，我们还能做什么？此外，他们没有对他们的算法提供太多解释。
stackoverflow.com/questions/5811635/dpll-algorithm-definition
@KristopherMicinski，你的博文现在是在一个新的 URL 上吗？

标签： algorithm logic artificial-intelligence

【解决方案1】：

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

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

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

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

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

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

我们已经分配了：

x1=true, x4=true

那么(~x1 \/ ~x4 \/ x5)是一个单元子句，因为你必须分配x5=true才能在当前的部分赋值中满足这个子句。

算法的基本思想是：

“猜”一个变量
查找从上次赋值创建的所有单元子句并分配所需的值
反复重试第 2 步，直到没有变化（找到传递闭包）
如果当前赋值不能为所有子句产生真值 - 从递归中折回并重试不同的赋值
如果可以 - “猜测”另一个变量（递归调用并返回 1）

终止：

无处可“返回”并更改“猜测”（无解决方案）
满足所有子句（有解决方案，算法找到了）

您还可以查看these lecture slides 了解更多信息和示例。

用法示例和重要性：
DPLL 尽管已有 50 年历史，但仍然是大多数 SAT 求解器的基础。
SAT 求解器对于解决难题非常有用，这是软件验证中的一个示例 - 您将模型表示为一组公式，以及您想要验证的条件 - 并在其上调用 SAT 求解器。虽然是指数级最坏情况——平均情况足够快并且在业界被广泛使用（主要用于验证硬件组件）

【讨论】：

“主要用于验证硬件组件”——并非完全正确。 DPLL 构成了任何 SMT 求解器的基础，它在静态分析软件中看到比硬件验证更广泛的使用（按人数计算）。尽管他们在硬件行业看到的应用比软件行业更多，这当然是真的！
如果我没记错的话，x1=false，x4=false 不应该吗？如果其中一个为真，则该子句已经满足？
@MaxB 我对迭代局部搜索（ILS）并不熟悉，但是从维基百科文章中我可以理解的一点是：（1）ILS用于优化问题，而DPLL用于SAT，是决策问题。 (2) ILS 是关于如何重启 (IIUC)，而 DPLL 是关于如何加快每次尝试。 (3) DPLL 已经有将近 60 年的历史了，而 wikipedia 中对 ILS 的参考是从 1995 年开始的，所以如果有的话 - ILS 源自 DPLL :)
请更新链接

【解决方案2】：

我会注意到，DPLL 中使用的技术是复杂性理论证明中常用的技术，您猜测对事物的部分赋值，然后尝试填写 em> 其余的。有关 DPLL 为何以这种方式工作的更多参考资料或灵感，您可以尝试阅读一些围绕 SAT 的复杂性理论材料（在任何关于复杂性理论的优秀教科书中）。

使用“现成”的 DPLL 实际上会导致一个非常糟糕的解决方案，并且您可以使用一些关键技巧来做得更好！除了 Amit 的回答，我将提供一些实际参考，以了解 DPLL 是如何工作的：

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

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

【讨论】：