如何在C++中最佳实现DPLL算法？

Question

我正在尝试在C++中实现DPLL算法，我想知道哪种数据结构最适合解决这种递归问题。目前我正在使用向量，但代码又长又丑。有什么建议吗？

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

- Mark

Answer 1

数组适合表示当前的分配情况，因为它可以随机访问任何命题。要表示子句，可以使用STL中命题索引的集合。

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

- user118967