文章/答案/技术大牛

发布

社区首页 >问答首页 >DPLL什么是一组一致的文字？

问DPLL什么是一组一致的文字？
EN

Stack Overflow用户

提问于 2017-11-02 15:40:39

回答 1查看 646关注 0票数 1

我正在编写一个SAT解算器，我开始实现一个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));

Φ是一组一致的文字，这是什么意思？我理解不一致意味着假，这意味着一致性并不意味着虚假。那么，如果当前的分配没有伪造问题，为什么我们可以返回true呢？

我实现SAT求解器的方式是，每当遇到使所有子句变为真的赋值时，我就返回该赋值，算法就完成了。但是对于给定的赋值，为了使它能够解决问题，所有的子句都必须是真的，我不明白，如果赋值true 满足问题(我假设这里有问题，但是如果Φ是一致的，那么它就意味着它不是假的，但它仍然是不可分辨的)。

algorithm

sat

sat-solvers

dpll

回答 1

Stack Overflow用户

回答已采纳

发布于 2017-11-02 17:22:28

Φ是一组一致的文字，如果它只包含文字和文字，并且它的否定不出现在Φ中。DPLL算法通过纯规则和单位规则，逐步将子句列表转换为满足所有原始子句的文本列表。当发生这种情况时(Φ是一组一致的文字)，或者当它用尽文字赋值来尝试，并且最顶层的DPLL调用返回false时，就会执行该算法。

票数 2

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

原文链接：

https://stackoverflow.com/questions/47079252

复制

相似问题

问DPLL什么是一组一致的文字？
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL什么是一组一致的文字？EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL什么是一组一致的文字？
EN