DPLL 算法

DPLL 是带可靠剪枝的二叉搜索。一次决策提出临时假设，单位传播把这项假设的全部显然代价结清；若账目出现矛盾，就回到最近尚有另一选择的岔路。算法不是随意试值：每个被剪分支都有一条被全部证伪的子句作为局部证明，而最终 UNSAT 表示两种极性递归形成的整棵有限树都已关闭。

它是回溯法公理库回溯法Backtracking深度优先枚举部分解并在不可能完成时撤销选择的搜索范式。在命题约束上的具体化。撤销必须覆盖该决策层之后的所有传播赋值，却不能删除更早层的事实。变量选择与先试极性可以极大改变树大小，但只要两个分支最终都能被探索，它们不改变判定结果。

令

根层没有单位子句。先决策 $x=1$：第三子句变成 $(y)$，第四子句变成 $(\mathrm{\neg }y)$，传播立即冲突。算法撤销这一层并尝试 $x=0$；此时第一子句要求 $y=1$，第二子句要求 $y=0$，再次冲突。$x$ 的两个取值已经覆盖全部总赋值，故返回 UNSAT。若只尝试第一个极性便停止，“没找到模型”仍不是证明。

纯文字消去有时列入 DPLL：若变量只以 $x$ 出现，可令 $x=1$ 满足所有相关子句。它保持“是否存在模型”，但会丢掉另一极性下的部分模型，因此在模型计数或枚举中不能无条件使用。另一个边界是最坏树大小仍可指数级；聪明分支只改善实例表现，不把一般 SAT 变成已知多项式算法。

DPLL 的搜索树与树形归结公理库树形归结Tree-like resolution每个导出子句至多被后续一步使用、因而证明依赖图为树的归结限制。有紧密对应：无学习回溯反复证明各分支冲突，不能跨分支复用已导出的子句。这一对应可把某些证明大小下界转成特定 DPLL 模型的运行时间下界，但不能约束拥有学习、预处理或专用理论推理的所有求解器。

CDCL公理库冲突驱动子句学习Conflict-driven clause learning · CDCL · Clause-learning SAT solving从传播冲突中推导原公式蕴涵的新子句，并据此非时序回跳和继续搜索的 SAT 算法。保留 DPLL 的决策与传播骨架，却分析冲突、学习由原式蕴涵的子句并非时序回跳。工程上还会加入增量求解、assumption literals 和模型重构；这些机制都必须维持同一搜索不变量：任何被永久排除的赋值都已由输入及有效学习子句证明不可能。