How to best implement DPLL in C++?
<p>I am trying to implement <a href="http://en.wikipedia.org/wiki/DPLL_algorithm#The_algorithm" rel="nofollow">DPLL</a> 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?</p>

<pre><code>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));
</code></pre>
