c++ - 如何在 C++ 中最好地实现 DPLL？

Question

我正在尝试实现 DPLL C++ 中的算法，我想知道哪种数据结构最适合解决此类递归问题。现在我正在使用 vector ，但代码又长又难看。有什么建议吗？

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

Answer 1

数组非常适合表示当前作业，因为它提供了对任何命题的随机访问。为了表示子句，可以使用 STL 的命题索引集。

要实现一个非常高效的 SAT 求解器，您将需要更多的数据结构(用于存储监视的文字和解释)。可以在 http://poincare.matf.bg.ac.rs/~filip/phd/sat-tutorial.pdf 找到对这些概念的非常易读的介绍。 .