提高DPLL算法的性能

Question

我正在实现a dpll 在C 中的算法，如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 分配为真时，您将标记所有包含 x 的正面字面的子句为无活动（并在此后忽略它们）并删除 -x 来自所有包含它的子句。记录哪些条款在其中具有 -X ，以便您以后可以回溯。还要记录您标记为不活动的哪个条款，出于相同的原因。

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

。

我在上面写了"少幼稚"，因为仍然有更好的方法。现代DPLL型SAT求解器使用懒惰的子句更新方案，称为"两个观察文字"，其优势是不需要从条款中删除文字，因此在发现不良的作业时不需要还原它们。仍然必须记录和回溯变量分配，但是不必更新与子句相关的结构的更新，使两个观察的文字比其他任何已知的SAT求解器的回溯方案都快。毫无疑问，您将在班上稍后了解这一点。