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?

@Eloff well, that would pretty much be giving away the code to my classmates on their first google search so I might get into trouble. Besides I was more hoping for something algorithmic, I can work on the implementation myself.. — none, Oct 25 '12 at 00:45

Kyle Jones · Accepted Answer · 2012-10-25T19:33:16.043

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.

marking inactive sounds interesting but I suppose I'm gonna also need to differentiate between different call levels since this is a recursive algorithm. btw do you happen to remember how feasible a naive algorithm is? mine can barely solve problems with 100 variables with 300+ clauses of length 3 in about 1 min, is that reasonable? — none, Oct 25 '12 at 12:50
That kind of performance is in line with what I would expect, but performance can vary wildly on the same SAT instance depending on the variable assignment order and other factors. — Kyle Jones, Oct 25 '12 at 18:21

improving performance of a dpll algorithm

1 Answers1