4

如维基百科中所述，我正在 C++ 中实现DPLL算法：

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));

目前我试图避免创建副本，Φ而是添加lornot(l)到一个且唯一的副本，并在 /if的 returnΦ时删除它们。这似乎破坏了给出错误结果的算法（即使集合是）。DPLL()falseUNSATISFIABLESATISFIABLE

有关如何在此步骤中避免显式复制的任何建议？

4

1 回答 1

1

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

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

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

于 2012-10-25T06:30:39.810 回答