0

我有以下条款：

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}

我必须分别使用 DP 和 DPLL 来证明可满足性。问题是我对每种算法都得到了不同的结果。带DP：

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}
6. {Q} from 1 and 2

2. {~P,R}
3'. {P,S}
4'. {~P,~R}
5. {P,~S}
7. {P} from 3' and 5

2. {R}
4'. {~R}
8. {}

所以是不能满足的。但是使用 DPLL：

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}
6. {P} split(P)

2'. {R}
4'. {Q,~R}

7.{Q}

这意味着它是令人满意的......我做错了什么？

4

1 回答 1

1

在 DP 的第一次推理中，解析规则没有正确应用。6. {Q} from 1 and 2让我们重点关注from1. {P,Q,~R}和的推断2. {P,Q,~R}。将 P、Q 和 R 分配给 false 满足{P,Q,~R}和{~P,R}，但它不满足{Q}前两个推论所要求的推理。{P,Q,~R}和的可能解决方案{~P,R}是：

  • {Q, ~R, R}通过解决P
  • {P, Q, ~P}通过解决R

这两个子句总是正确的并且被 DP 丢弃。（丢弃有时被称为重言式规则。）这些并不必然{Q}如前面的反例所示。

另请注意，在 DPLL 示例中，您已将 P、R、Q 分配为真。这与从句不一致4. {~P,~Q,~R}。需要对这种拆分进行详尽的单元传播。

您可以在网上找到许多关于 DP 和 DPLL 的演示文稿。示例：1、2。尝试一致且详尽地应用这些规则。

于 2021-01-23T22:14:21.717 回答