DPLL算法程序答案

【问题标题】：DPLL algorithm procedureDPLL算法程序
【发布时间】：2017-05-06 20:03:56
【问题描述】：

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

【问题讨论】：

【解决方案1】：

该步骤不会以这种方式发生，因为输入中有单元子句会首先被解析。

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

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

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

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

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

【讨论】：

那么，当我看到单元子句时，我的第一步应该是什么？
如果c 变为 1，那么 C7 将是 {} 或 {1} ?
@nirvair C7 将是 {1}，但由于它包含 {1}，它将变为非活动状态。当你有一个单元时，进行单元传播。
我还没有真正理解单元传播是如何工作的。
从概念上讲，用 1 代替积极使用，用 0 代替消极使用，然后简化（从子句中删除 0，删除包含 1 的子句）。实际上它不会那样工作，因为天真地这样做会花费太多的数据结构，它会很慢。如果您认真考虑编写 SAT 求解器，您可能应该查看文献，这是一个很大的主题。