如何在 C++ 中最好地实现 DPLL?
Posted
技术标签:
【中文标题】如何在 C++ 中最好地实现 DPLL?【英文标题】:How to best implement DPLL in C++? 【发布时间】:2012-03-29 04:31:14 【问题描述】:我正在尝试在 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));
【问题讨论】:
【参考方案1】:数组非常适合表示当前分配,因为它提供对任何命题的随机访问。为了表示从句,可以使用 STL 的命题索引集。
要实现一个非常高效的 SAT 求解器,您需要更多的数据结构(用于存储观察到的文字和解释)。可以在http://poincare.matf.bg.ac.rs/~filip/phd/sat-tutorial.pdf 找到对这些概念的非常易读的介绍。
【讨论】:
以上是关于如何在 C++ 中最好地实现 DPLL?的主要内容,如果未能解决你的问题,请参考以下文章