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));
+3
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 .
0
source to share