我正在尝试在C++中实现DPLL算法,我想知道哪种数据结构最适合解决此类递归问题。现在我正在使用 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));

最佳答案

数组可以很好地表示当前任务,因为它可以随机访问任何命题。为了表示从句,可以使用STL的命题索引集。

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

08-25 08:06