DPLL算法定义答案

【问题标题】：DPLL algorithm definitionDPLL算法定义
【发布时间】：2011-04-27 22:57:49
【问题描述】：

我在理解 DPLL 算法时遇到了一些问题，我想知道是否有人可以向我解释，因为我认为我的理解不正确。

我理解它的方式是，我采用一些文字，如果某些每个子句为真，则模型为真，但如果某些子句为假，则模型为假。

我通过寻找一个单元子句递归地检查模型，如果有，我设置该单元子句的值以使其为真，然后更新模型。删除所有现在为真的子句并删除所有现在为假的文字。

当没有剩余单元子句时，我选择了任何其他文字并为该文字分配值，使其为真并使其为假，然后再次删除所有现在为真的子句和所有现在为假的文字。

【问题讨论】：

老实说，我看不出这个问题与以前的问题有何不同，或者添加了其他任何内容。看起来您已经阅读了第 n+1 个答案，现在终于感到满意，但这对我来说仍然是重复的。

标签： algorithm artificial-intelligence

【解决方案1】：

DPLL 要求问题以析取范式表示，即作为一组子句，每个子句都必须满足。

每个子句都是一组文字 {l1, l2, ..., ln}，表示这些文字的析取（即，至少一个文字必须为真才能满足子句）。

每个文字 l 断言某个变量为真 (x) 或为假 (~x)。

如果子句中的任何文字为真，则该子句得到满足。

如果一个子句中的所有文字都是假的，那么该子句是不可满足的，因此问题是不可满足的。

解决方案是将真/假值分配给变量，以便满足每个子句。 DPLL 算法是对此类解决方案的优化搜索。

DPLL 本质上是一种在三种策略之间交替进行的深度优先搜索。在搜索的任何阶段都有一个部分赋值（即对变量的某个子集赋值）和一组未定子句（即那些尚未满足的子句）。

(1) 第一种策略是纯字面量消除：如果一个未赋值变量x 只以正数形式出现在未定子句集中（即字面量~x 没有出现在任何地方），那么我们可以只需将x = true 添加到我们的赋值中并满足包含文字x 的所有子句（类似地，如果x 仅以否定形式出现，~x，我们可以将x = false 添加到我们的赋值中）。

(2) 第二种策略是单元传播：如果未定子句中除了一个文字之外的所有文字都是假的，那么剩下的就一定是真的。如果剩下的文字是x，我们将x = true添加到我们的赋值中；如果剩下的文字是~x，我们将x = false 添加到我们的赋值中。这种分配可以为单位传播带来更多机会。

(3) 第三种策略是简单地选择一个未分配的变量x 并分支搜索：一侧尝试x = true，另一侧尝试x = false。

如果在任何时候我们最终得到一个不可满足的子句，那么我们已经走到了死胡同，不得不回溯。

还有各种巧妙的进一步优化，但这是几乎所有 SAT 求解器的核心。

希望这会有所帮助。

【讨论】：

很好的解释。 OP 的问题表明他/她可能遗漏了您的第三种策略是“暂定的”——即在这种情况下，我们在概念上需要在尝试一项任务之前“保存”并准备“恢复”并尝试其他任务以防万一下游失败。（虽然 OTOH 策略 1 和 2 始终有效并且永远不需要撤消，除非它们发生在使用策略 3 之后，而策略 3 本身需要撤消。）
@j_random_hacker，你的意思是对于第 3 部分，你先尝试假然后再尝试真，而不是真假？你怎么知道哪些该保留哪些该忽略？
@Rafe，你说如果在任何时候我们最终得到一个不可满足的子句，那么我们必须回溯，但之前你说如果有一个不可满足的子句，那么问题就是不可满足的，即它？我有点困惑。谢谢。
... 如果不是，但可以应用规则 3，假设变量 x，我们任意选择一个值（例如“true”）并在末尾添加一个包含 x=true 的新状态的链表。但是在添加这个新状态之前，我们在当前节点上贴了一张便利贴，上面写着“Try x=false”。便利贴的目的是：每当我们到达一个包含不可满足条款的状态时，我们不会立即放弃，而是开始爬上链表寻找便利贴。如果我们在没有找到的情况下到达顶峰，那么我们会说“它无法满足！”。但如果我们真的找到了……
... 在爬上链表时，我们立即停止并按照便利贴上的说明进行操作 - 即我们此时恢复搜索，在底部添加另一个节点做出与我们第一次做相反的选择。一旦我们开始按照它所说的去做，我们就会把便利贴扔进垃圾箱。如果您在纸上尝试一些玩具示例，您应该能够说服自己这将始终做正确的事情，并且最终总是会终止。

【解决方案2】：

Davis-Putnam-Logemann-Loveland (DPLL) 算法是一种基于回溯的搜索算法，用于确定合取范式中命题逻辑公式的可满足性，也称为可满足性问题或 SAT。

任何布尔公式都可以用合取范式（CNF）表示，这意味着从句的合取，即（…）^（…）^（…）

其中一个子句是布尔变量的析取，即 (A v B v C' v D)

一个用 CNF 表示的布尔公式的例子是

(A v B v C) ^ (C' v D) ^ (D' v A)

解决 SAT 问题意味着找到公式中满足它的变量的值组合，例如 A=1、B=0、C=0、D=0

这是一个 NP 完全问题。实际上这是 Stepehn Cook 和 Leonid Levin 证明是 NP-Complete 的第一个问题

一种特殊类型的 SAT 问题是 3-SAT，它是一个所有子句都有三个变量的 SAT。

DPLL 算法是解决 SAT 问题（实际上取决于输入的难度）的方法，它递归地创建潜在解决方案树

假设你想像这样解决一个 3-SAT 问题

(A v B v C) ^ (C' v D v B) ^ (B v A' v C) ^ (C' v A' v B')

如果我们枚举 A=1 B=2 C=3 D=4 之类的变量，并为 A' = -1 之类的否定变量设置负数，那么可以像这样在 Python 中编写相同的公式

[[1,2,3],[-3,4,2],[2,-1,3],[-3,-1,-2]]

现在想象创建一棵树，其中每个节点都包含一个部分解决方案。在我们的示例中，我们还描述了解决方案满足的子句向量

根节点是 [-1,-1,-1,-1] 这意味着尚未为既不是 0 也不是 1 的变量分配任何值

每次迭代：

然后我们取第一个不满足的子句

请看下面的例子：

我们从根节点选择第一个子句 (A v B v C) 的第一个变量 (A) 并将其设置为满足子句然后 A=1（搜索树的第二个节点）

继续第二个子句，我们选择第一个未分配的变量 (C) 并将其设置为满足子句，即 C=0（左侧第三个节点）

我们对第四个子句（B v A' v C）做同样的事情，并将 B 设置为 1

我们尝试对最后一个子句做同样的事情，我们意识到我们不再有未分配的变量并且该子句总是错误的。然后我们必须回溯到搜索树中的前一个位置。我们改变分配给 B 的值，并将 B 设置为 0。然后我们寻找另一个可以满足第三个子句但不存在的未分配值。然后我们又要回溯到第二个节点

在那里，我们必须翻转第一个变量 (C) 的赋值，使其不满足子句并设置下一个未赋值变量 (D) 以满足它（即 C=1 和 D=1 ）。这也满足包含 C 的第三个子句。

要满足的最后一个子句 (C' v A' v B') 有一个未分配的变量 B，然后可以将其设置为 0 以满足该子句。

在这个链接http://lowcoupling.com/post/72424308422/a-simple-3-sat-solver-using-dpll你也可以找到实现它的python代码

【讨论】：