DPLL算法如何工作？
Gho*_*ost 9 algorithm logic artificial-intelligence
该算法取自人工智能现代方法.我发现这很多功能递归真的很混乱.特别是,EXTEND()函数做了什么,递归调用的目的是DPLL()什么？
ami*_*mit 16
该DPLL本质上是一种回溯算法,这就是递归调用背后的主要思想.
该算法在尝试分配时构建解决方案,您有一个部分解决方案可能会证明您成功或不成功.算法的天赋是如何构建部分解决方案.
首先,让我们定义一个单元子句:
单元子句是一个子句,它只有一个文本仍然是未分配的,而另一个(赋值的)文字 - 都被赋值为false.
此子句的重要性在于,如果当前赋值有效 - 您可以确定未赋值文字中变量的值是什么 - 因为文字必须为true.
例如:如果我们有一个公式:
(x1 \/ x2 \/ x3) /\ (~x1 \/ ~x4 \/ x5) /\ ( ~x1 \/ x4)
我们已经指定:
x1=true, x4=true
然后(~x1 \/ ~x4 \/ x5)是一个单元子句,因为必须分配x5=true才能在当前的部分赋值中满足该子句.
该算法的基本思想是:
- "猜猜"变量
- 查找从上次分配创建的所有单元子句并分配所需的值
- 迭代重试步骤2,直到没有变化(找到传递闭包)
- 如果当前赋值不能为所有子句生成true - 从递归折回并重试另一个赋值
- 如果可以 - "猜测"另一个变量(递归调用并返回1)
终止:
- 没有地方可以"回到"并改变"猜测"(没有解决方案)
- 满足所有条款(有一个解决方案,算法找到了)
您还可以查看这些演讲幻灯片以获取更多信息和示例.(忽略第一张希伯来语幻灯片,接下来都是英语;你可能也想忽略最后的"学习",直到你更好地理解基础知识)
用法示例和重要性:
DPLL虽然已有50年历史,但仍然是大多数SAT求解器的基础.
SAT求解器对于解决难题非常有用,软件验证中的一个例子 - 您将模型表示为一组公式,以及您要验证的条件 - 并通过它调用SAT求解器.虽然指数最坏的情况 - 平均情况足够快并且在业界广泛使用(主要用于验证硬件组件)
我会注意到，DPLL 中使用的技术是复杂性理论证明中常用的技术，您猜测事物的部分分配，然后尝试填写其余部分。有关为什么 DPLL 以这种方式工作的更多参考或灵感，您可以尝试阅读一些围绕 SAT 的复杂性理论材料（在任何关于复杂性理论的好教科书中）。
使用“现成的”DPLL 实际上会导致一个非常糟糕的解决方案，并且您可以使用一些关键技巧来做得更好！随着 Amit 的回答，我将提供一些实用的参考资料，以了解真实的 DPLL 是如何工作的：
- 如果我们有很多变量的公式
{x1,...,xn}，你会发现，DPLL算法将终止更加迅速（在该公式的情况下是根据符合要求），其选择的变量。您还会发现正确选择（显然）更有帮助。 - 有多种技术可以帮助您做到这一点，称为变量选择启发式。
- 还对公式的表示进行了许多优化，以便您可以快速传播决策和饱和子句，特别是“两个观察文字”技术。
- 在真正的SAT的突破是基于条款的学习。每当您“卡住”时，您就会创建一个新子句以添加到您的数据库中，这将阻止您搜索空间中“无用”的区域。已经有很多关于包含学习从句的最佳策略的研究：应该包含哪些，以及何时包含？
- MiniSat是一个现实的和高度优化的 SAT 求解器。我发现Original MiniSat 论文在弄清楚如何进行真正最佳的 SAT 求解方面确实令人大开眼界。这真的是一本很棒的读物，如果您有兴趣了解有关可靠 SAT 求解器实现的更多信息，强烈建议您阅读。
因此，从理论上讲，SAT 的核心是一个非常重要的问题（通过 Karp 进行的第一个 NP 完全约简，任何复杂性书籍都会介绍的有趣而乏味的构造技术），但在模型检查和软件验证方面也有非常实际的应用。如果您对如何快速解决 NP 完全问题的经典示例感兴趣，请查看工业强度 SAT 求解器的实现，这很有趣！