问DPLL算法定义

EN

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

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

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

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

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

解决方案是将true/false值赋给变量，以便满足每个子句。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求解器的核心。

希望这能有所帮助。

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

任何布尔公式都可以用合取范式来表示，合取范式表示子句的合取，即(…)^(…)^(…)

其中一个子句是布尔变量的析取，即(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完全的第一个问题

一种特殊类型的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，-1,3，-3，-1，-2]

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

根节点是-1、-1、-1、-1，这意味着尚未为变量0或1赋值

在每次迭代中：

如果没有更多的未赋值变量可以用来满足该子句，那么在搜索树的这个分支中就不可能有有效的解，算法应该返回None

• ，否则我们取第一个未赋值的变量，并设置它，使其满足该子句，并从步骤1递归开始。如果算法的内部调用返回None，我们反转该变量的值，使其不满足该子句，并设置下一个未赋值的变量，以满足该子句。如果所有三个变量都已尝试，或者该子句不再有未赋值的变量，则意味着此分支中没有有效的解决方案，算法将返回None

请参见以下示例：

从根节点中，我们选择第一个子句(A、B、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代码