问DPLL算法是如何工作的？

EN

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

算法是在尝试分配的同时构建解决方案，随着时间的推移，你会得到一个可能成功或不成功的部分解决方案。算法的精巧之处在于如何构造局部解。

首先，让我们定义一下什么是单位子句：

unit子句是这样一个子句，它恰好有一个未赋值的文字，而其他(已赋值的)文字都被赋值为false。

这个子句的重要性在于，如果当前赋值是有效的-您可以确定未赋值文字中的变量的值是什么-因为文字必须为true。

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

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

我们已经分配了：

x1=true, x4=true

那么(~x1 \/ ~x4 \/ x5)就是一个unit子句，因为您必须赋值x5=true，以便在当前的部分赋值中满足这个子句。

算法的基本思想是：

如果当前赋值不能为所有子句生成true -从递归返回并重试不同的assignment

• If，则“”

2. 可以- "guess“另一个变量(递归调用并返回到1)

Termination:

没有地方可以“返回”并更改“solution)

• All”(没有子句被满足(存在一个解决方案，并且算法找到了它)

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

：用法示例和重要性

虽然DPLL已经有50年的历史了，但它仍然是大多数SAT求解器的基础。

SAT求解器对于解决困难问题非常有用，软件验证中的一个示例-将模型表示为一组公式和要验证的条件-并在其上调用SAT求解器。虽然指数最坏情况-平均情况是足够快的，并在行业中广泛使用(主要用于验证硬件组件)

我要指出的是，DPLL中使用的技术是复杂性理论中证明中使用的常见技术，您可以猜测对事物的部分赋值，然后尝试填充其余部分。要获得更多关于DPLL为什么会这样工作的参考资料或灵感，您可以尝试阅读一些围绕SAT的复杂性理论材料(在任何关于复杂性理论的优秀教科书中)。

使用DPLL“现成的”实际上导致了一个相当糟糕的解决方案，并且有一些关键技巧可以让你做得更好！伴随着Amit的回答，我将给出一些实际的参考，以理解DPLL是如何工作的：

如果我们有一个包含多个变量的公式，你会发现

• 算法的终止速度会快得多(在公式可满足的情况下)，这取决于你选择的变量。你还会发现正确的选择(显然)更有帮助。
• 有多种技术可以帮助你做到这一点，称为variable selection heuristics.
• There。在公式的表示中也有许多优化，这样你就可以快速传播决策并饱和子句，特别是“两个观察到的字面”技术。
• SAT中真正的突破是基于子句学习。每当您遇到“卡住”的情况时，您都会创建一个新的子句来添加到数据库中，这将阻止您搜索空间中的“无用”区域。已经有很多关于包含学习到的子句的最佳策略的研究:应该包括哪些，而when?
• MiniSat是一个现实的、高度优化的SAT求解器。我发现Original MiniSat paper真的让我大开眼界，让我知道如何做最优的SAT求解。这真的是一本很棒的书，如果你有兴趣了解更多关于可靠的SAT求解器的实现，强烈推荐你。

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