一个完备的回溯搜索

7.6.1 一个完备的回溯搜索

我们考虑的第一个算法通常被称为戴维斯-普特南（Davis-Putnam）算法，以Martin Davis和Hilary Putnam（1960）的开创性论文命名。实际上，该算法是 Davis、Logemann 和 Loveland （1962）描述的版本，因此我们按最初的这4个作者首字母缩写将其命名为DPLL。DPLL把合取范式形式的一个语句——子句集——作为输入。如同BACKTRACKING-SEARCH和TT-ENTAILS?，它本质上也是一个对可能模型的递归深度优先枚举算法。相对于TT-ENTAILS?的简单方法，它具有以下3个方面的改进：

• 及早终止：算法检测该语句是否一定为真或为假，即使对部分完成的模型也不例外。如果一个子句的任一文字为真，那么该子句也为真，即使其它文字还没有设定真值；因此，作为一个整体的语句甚至在模型完成之前就可以判定为真。例如，如果A为真，那么语句(A∨B)∧(A∨C)为真，与B和C的值无关。类似地，如果任一条子句为假，那么该语句为假。再次，这种情况可以发生在模型完成之前很早的时候。及早终止避免了对搜索空间全部子树的检查。

• 纯符号启发式：纯符号是在所有子句中以相同“正负号”出现的一个符号。例如，在这3个子句(A∨¬B)，(¬B∨¬C)和(C∨A)中，A 为纯符号，因为只有正文字出现，B 为纯符号因为它只有否定文字，而C是非纯的。很容易看出，如果某个语句具有一个模型，那么它就一定有一个纯符号构成的模型以便使得它们的文字为 true，因为这样的做法永远不会使得一个子句的值变为假。需要注意，在检验符号的纯度时，本算法可以忽略自模型开始构造以来已知为真的子句。例如，如果模型包括B = false，那么子句(¬B∨¬C)已经为真，而C变成纯符号，因为它只在(C∨A)中出现。

• 单元子句启发式：单元子句先前已经定义为只有一个文字的子句。在DPLL的背景下，它还表示这样的子句，即除某个文字以外的所有其它文字都被模型赋值为false。例如，如果模型包括B = false，那么(B∨¬C)成为一个单元子句，因为它等价于(False∨¬C)，或者说就是¬C。

显然，如果要求这个子句为真，那么对C的赋值必须为false。单元子句启发式在余下的部分出现分支前，对所有这样的符号进行赋值。单元子句启发式的一个重要结果是，任何试图对已经存在于知识库中的一个文字进行证明（通过反证）的做法将立即取得成功（习题7.16）。

还需要注意，对某个单元子句的赋值可能生成另一个单元子句——例如，C被置为false，(C∨A)成为一个单元子句，致使把A赋值为true。这种强制赋值的“串联”称为单元传播。它与霍恩子句的前向链接过程类似，而且实际上，如果 CNF 表达式中只包括霍恩子句，那么DPLL本质上重复了前向链接。（参见习题7.17。）

DPLL算法如图7.16所示。我们已经给出了算法的基本骨架，它描述了搜索过程自身。我们没有描述为了使得每个搜索步骤有效率而必须维护的数据结构，也没有介绍可以用于提高性能的诀窍：子句学习、变量选择启发式和随机重新开始。将所有这些内容包括进来以后，尽管DPLL比较古老，但是它仍然是已开发的最快的满足性算法之一。其CHAFF实现被用来解决百万个变量的硬件校验问题。

图7.16 用于检验命题逻辑语句的可满足性的DPLL算法。FIND-PURE-SYMBOL和FIND-UNIT-CLAUSE在教材中进行了描述；每个函数都返回一个符号（或空值null）和赋予该符号的真值。如同TT-ENTAILS?，它只对不完全模型进行操作