DPLL算法

在逻辑学和计算机科学中，（DPLL）算法是一种完整的、基于回溯的搜索算法，用于决定共轭正常形式下命题逻辑公式的可满足性，即用于解决CNF-SAT问题。

SAT问题从理论和实践的角度来看都很重要。在复杂性理论中，它是xxx个被证明是NP-complete的问题，并且可以出现在各种各样的应用中，如模型检查，自动计划和调度，以及人工智能的诊断。因此，编写高效的SAT求解器已经是一个多年的研究课题。

基本的回溯算法通过选择一个字面，给它分配一个真值，简化公式，然后递归检查简化后的公式是否可满足；如果是这样，原公式是可满足的；否则，假设真值相反，进行同样的递归检查。这被称为分割规则，因为它将问题分割成两个更简单的子问题。简化步骤实质上是将所有在赋值下成为真值的子句从公式中移除，并将所有成为假值的字词从剩余子句中移除。DPLL算法通过在每一步急切地使用以下规则来加强对反向追踪算法的支持。

如果一个子句是一个单位子句，即它只包含一个未分配的字词，这个子句只能通过分配必要的值使这个字词为真来满足。因此，没有必要进行选择。单元传播包括删除每一个包含单元子句字样的子句，以及从每一个包含单元子句字样的子句中丢弃该补码。在实践中，这往往会导致确定的单元级联，从而避免了很大一部分天真的搜索空间。纯粹字面消除如果一个命题变量在公式中只出现一个极性，那么它就被称为纯粹的。纯粹的字面意义总是可以以一种方式分配，使包含它的所有子句都为真。因此，当它以这种方式被赋值时，这些子句不再限制搜索，可以被删除。

如果一个子句变成空的，也就是说，如果它的所有变量被分配的方式使相应的字词变成了假的，那么就可以检测到一个给定的部分赋值的不可满足性。公式的可满足性在所有变量都被赋值而不产生空子时被检测出来，或者在现代的实现中，所有子句都被满足。完整公式的不满足性只有在穷举搜索后才能被检测出来。DPLL算法可以总结为以下的伪代码，其中Φ是CNF公式。

DPLL输入。一组子句Φ。输出。一个表示Φ是否可满足的真值。函数DPLL(Φ)当Φ中存在一个单元句{l}时，Φ←单元传播(l,Φ)；当Φ中存在一个纯文本l时，Φ←纯文本分配(l,Φ)。如果Φ是空的，则返回true；如果Φ包含一个空的子句，则返回false；l←选择字词(Φ)；分别返回对字词l和公式Φ应用单元传播和纯字词规则的结果。返回语句中的or是一个短路运算符。Φ∧{l}表示在Φ中用真代替l的简化结果。该算法在两种情况中的一种终止。要么CNF公式Φ是空的，即它不包含任何子句。那么它可以被任何赋值所满足，因为它的所有子句都是空的真。