如何在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)); 

Answer 1

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

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