我在理解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()的目的是什么？

回答：

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

算法在尝试分配的同时构建解决方案，您有一个部分解决方案，可能会成功或不成功。算法的巧妙之处在于如何构建部分解决方案。

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

单元子句是一个子句，它只有一个未分配的文字，而其他已分配的文字都分配为假。这个子句的重要性在于，如果当前分配是有效的 – 您可以确定未分配文字中变量的值 – 因为该文字必须为真。

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

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