What's the best way to implement DPLL in C ++?

I am trying to implement DPLL algorithm in C ++, I am wondering which data structure would be better for solving this type of recursion problem. Right now I am using vectors, but the code is long and ugly. Are there any suggestions?

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));



source to share

1 answer

An array is good for representing the current assignment as it allows random access to any of the clauses. To represent sentences, you can use STL sets of sentence indices.

To implement a very efficient SAT solution, you need a few more data structures (for storing scanned literals and explanations). A very readable introduction to these concepts can be found at http://poincare.matf.bg.ac.rs/~filip/phd/sat-tutorial.pdf .



All Articles