文章/答案/技术大牛

发布

社区首页 >问答首页 >DPLL算法程序

问DPLL算法程序
EN

Stack Overflow用户

提问于 2017-05-07 04:03:57

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

我正在尝试理解DPLL过程，然后才真正编码它。

例如，我有这些子句：

C1 : {c, !d, !b}    
C2 : {d, a}
C3: {b, !d, !a}    
C4: {d, c, b, a}    
C5: {c, !d, !b}    
C6: {d, c, b}    
C7: {c}

现在我把决策变量设为d= 0，b= 0。这个子句现在看起来像这样。

C1: {c, 1, 1}
C2: {a}
C3: {1, !a}
C4: {c, a}
C5: {c, 1, 1}
C6: {c}
C7: {c}

单元传播和纯文字规则在这里是如何发挥作用的？

另外，在C3 : {1, !a}中-当我使用a = 1时，它就变成了{1, 0}。这个子句的最终值应该是什么？是否应为{1}？

如果任何子句的值为{!b}，在应用决策变量之后，这是对文字的否定，那么如何继续呢？

algorithm

authentication

sat

satisfiability

dpll

回答 1

Stack Overflow用户

发布于 2017-05-07 04:49:08

这一步不会以这种方式发生，因为输入中有单位子句，这些子句将首先被解析。

{ c } (子句)是一个单位，它的文字c是正的，因此c (变量)被强制为1，然后我们有

C2 : {d, a}
C3: {b, !d, !a}

作为活动子句，因为true子句被忽略。

现在b是一个纯文字(它并不总是如此，但由于一些子句不再活动，它就变成了一个纯文字)，但实际的SAT解算器通常不会检查这一点，除非在预处理期间，因为它不能被有效地检查。

最后，您可以设置d或a，或者两者都设置，这并不重要。

票数 1

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

原文链接：

https://stackoverflow.com/questions/43824897

复制

相似问题

问DPLL算法程序
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL算法程序EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DPLL算法程序
EN