c++ - 改善dpll算法的性能

我正在wikipedia中描述的在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));

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

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

最佳答案

一种不太天真的DPLL方法避免通过在单元传播和纯文字分配步骤中记录变量分配和对子句所做的更改来复制公式，然后在生成空子句时撤消更改(回溯)。因此，当为变量x赋值为true时，您会将所有包含x的正文字的子句标记为不 Activity (由于满足了条件，此后将其忽略)，并从包含它的所有子句中删除-x。记录其中包含-x的子句，以便稍后回溯。出于相同的原因，还要记录您标记为不 Activity 的子句。

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

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