Improving the efficiency of the dpll algorithm

Question

I implement the 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 with terrible performance. In this step:

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

I'm currently trying not to make copies of Φ , but instead add l or not(l) to a single copy of Φ and delete them when / if DPLL() returns false . This seems to violate the algorithm giving the wrong results ( UNSATISFIABLE , although the set is SATISFIABLE ).

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

Answer 1

A less naive approach to DPLL allows you to avoid copying the formula by writing variable assignments and changes made to sentences in the units and pure literal allocation steps, and then undoing the changes (backtracks) when creating an empty sentence.Therefore, when x is set to true, you should mark all clauses containing the positive literal x as inactive (and ignore them after that, since they are executed), and remove -x from all sentences that contain it. Write down what sentences had -x in them so you can go back. Also write down the sentences that you marked inactive for the same reason.

Another approach is to track the number of unassigned variables in each unsatisfied sentence. Record when the number decreases, so you can go back. The propagation of one, if the counter reaches 1, is returned if the number reaches 0, and all literals are false.

I wrote the “least” above because there are even better approaches. Modern DPLL-type SAT solutions use a lazy sentence update scheme called "two scanned literals", which has the advantage of not having to remove literals from sentences and therefore not having to restore them when a bad assignment is detected. Assignment variables still need to be written and returned, but it does not require updating the structures associated with the proposal, making two literals scanned faster than any other known backtracking scheme for SAT solvers. You will undoubtedly learn about this later in your class.