improving performance of a dpll algorithm

Question

I'm implementing a DPLL algorithm in C++ as described in 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));

but having an awful performance. In this step:

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

currently I'm trying to avoid creating copies of Φ but instead adding l or not(l) to the one and only copy of Φ and remove them when/if DPLL()'s return false. This seems to break the algorithm giving wrong results (UNSATISFIABLE even though the set is SATISFIABLE).

Any suggestions on how to avoid explicit copies in this step?

Answer 1

A less naive approach to DPLL avoids copying the formula by recording the variable assignments and the changes made to the clauses in the unit-propagation and pure-literal assignment steps and then undoes the changes (backtracks) when an empty clause is produced. So when a variable x is assigned true, you would mark all clauses containing a positive literal of x as inactive (and ignore them thereafter since they are satisfied) and remove -x from all clauses that contain it. Record which clauses had -x in them so you can backtrack later. Also record which clauses you marked inactive, for the same reason.

Another approach is to keep track of the number of unassigned variables in each unsatisfied clause. Record when the number decreases so you can backtrack later. Do unit propagation if the count reaches 1, backtrack if the number reaches 0 and all the literals are false.

I wrote "less naive" above because there are still better approaches. Modern DPLL-type SAT solvers use a lazy clause updating scheme called "two watched literals" that has the advantage of not needing to remove literals from clauses and thus not needing to restore them when a bad assignment is found. The variable assignments still have to be recorded and backtracked, but not having to update the clause-related structures makes two watched literals faster than any other known backtracking scheme for SAT solvers. You'll no doubt learn about this later in your class.