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}吗？

如果任何子句具有 value {!b}，即对文字的否定，在应用决策变量之后，那么如何进行？

4

1 回答 1

1

该步骤不会以这种方式发生，因为输入中的单元子句将首先得到解决。

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

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

作为活动从句，因为真正的从句被忽略。

Nowb是一个纯文字（并非总是如此，但由于某些子句不再处于活动状态，它变成了一个），但实际的 SAT 求解器通常不会检查它，除非在预处理期间，因为它不能被有效地检查。

最后你会设置d或a两者都没有关系。

于 2017-05-06T20:49:07.923 回答