algorithm - DPLL算法流程

Question

我试图在实际编码之前了解 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}，即对文字的否定，在应用决策变量后，如何进行？

Answer 1

那一步不会那样发生，因为输入中的单元子句会先被解决。

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

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

作为事件子句，因为真正的子句会被忽略。

现在 b 是一个纯文字(它并不总是，但它变成了一个，因为一些子句不再活跃)，但实用的 SAT 求解器通常不会检查它，除非在预-处理，因为它不能被有效地检查。

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