文章/答案/技术大牛

发布

问一种改进dpll算法的性能
EN

Stack Overflow用户

提问于 2012-10-24 21:56:26

回答 1查看 1.5K关注 0票数 4

我正在用DPLL算法在C++中实现维基百科中的描述

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

但是表演很糟糕。在这一步骤中：

return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

目前，我试图避免创建Φ的副本，而是将l或not(l)添加到Φ的唯一副本中，并在DPLL()返回false时删除它们。这似乎破坏了给出错误结果的算法(UNSATISFIABLE，即使集合是SATISFIABLE)。

关于如何在此步骤中避免显式副本的建议吗？

recursion

sat-solvers

dpll

c++

algorithm

回答 1

Stack Overflow用户

回答已采纳

发布于 2012-10-25 06:30:39

不太天真的DPLL方法可以避免复制公式，方法是记录变量赋值和对单元传播和纯文字赋值步骤中的子句所做的更改，然后在生成空子句时取消更改(回溯)。因此，当变量x被赋值为true时，您将所有包含正字面值x的子句标记为非活动子句(然后忽略它们，因为它们满足)，并从包含它的所有子句中删除-x。记录哪些子句中包含-x，以便您稍后可以回溯。还要记录您出于同样的原因标记为非活动的子句。

另一种方法是跟踪每个不满意子句中未分配变量的数量。记录数字减少的时间，以便以后可以回溯。如果计数达到1，则执行单位传播；如果数达到0，则回溯，并且所有文字都是假的。

我在上面写了“不那么天真”，因为还有更好的方法。现代DPLL型SAT求解器使用一种名为“两个监视文本”的懒子句更新方案，它的优点是不需要从子句中删除文本，因此在发现错误分配时不需要恢复它们。变量分配仍然需要记录和回溯，但是不需要更新与子句相关的结构，这使得两个被监视的文本比任何已知的SAT求解器回溯方案都要快。毫无疑问，你以后会在课堂上了解到这一点的。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/13058438

复制

相似问题

问一种改进dpll算法的性能
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问一种改进dpll算法的性能EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问一种改进dpll算法的性能
EN