CODEWITHSUNDEEP
c++algorithmlogicartificial-intelligencedpll
Mark
Mark

Reputation: 8678

How to best implement DPLL in C++?

I am trying to implement DPLL algorithm in C++, I am wondering what kind of data structure would be best 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));

Upvotes: 4

Views: 3419

Answers (1)

user118967
user118967

Reputation: 5722

An array is good for representing the current assignment, as it provides random access to any of the propositions. To represent clauses, one can use STL's sets of the proposition indices.

To implement a very efficient SAT solver you will need some more data structures (for storing watched 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.

Upvotes: 2

Related Questions