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或不是(l)添加到Φ的唯一副本中,并在/当DPLL()返回false时将其删除.这似乎打破了算法给出错误的结果(UNSATISFIABLE,即使该集合是SATISFIABLE).

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