c++ - 提高 dpll 算法的性能

Question

我正在用 C++ 实现一个 DPLL 算法，如 wikipedia 中所述。 :

function DPLL(Φ)
   if Φ is a consistent set of literals
       then return true;
   if Φ contains an empty clause
       then return false;
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

但表现糟糕。在这一步中:

return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

目前我正在尝试避免创建 Φ 的拷贝，而是将 l 或 not(l) 添加到唯一的拷贝Φ 并在/如果 DPLL() 返回 false 时删除它们。这似乎破坏了给出错误结果的算法(UNSATISFIABLE，即使集合是 SATISFIABLE)。

关于如何在这一步避免显式复制有什么建议吗？

Answer 1

一种不太天真的 DPLL 方法通过记录变量赋值和在单元传播和纯文字赋值步骤中对子句所做的更改来避免复制公式，然后在生成空子句时撤消更改(回溯) .因此，当变量 x 被赋值为 true 时，您会将所有包含 x 的正文字的子句标记为不活动(并在之后忽略它们，因为它们已满足)并删除 -x 来自所有包含它的子句。记录哪些子句中包含 -x，以便稍后回溯。出于同样的原因，还要记录您将哪些条款标记为无效。

另一种方法是跟踪每个未满足子句中未分配变量的数量。记录数字减少的时间，以便稍后回溯。如果计数达到 1 则进行单元传播，如果数字达到 0 且所有字面量均为 false，则回溯。

我在上面写了“不那么天真”，因为还有更好的方法。现代 DPLL 类型的 SAT 求解器使用称为“两个监视文字”的惰性子句更新方案，其优点是不需要从子句中删除文字，因此在发现错误分配时不需要恢复它们。变量赋值仍然需要记录和回溯，但不必更新与子句相关的结构使得两个监视文字比 SAT 求解器的任何其他已知回溯方案更快。毫无疑问，您稍后会在类里面了解到这一点。