问题描述
我有以下条款：
1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~R}
5. {P,~S}
我必须分别使用DP和dplL证明可满足性。问题是我对每种算法都得到了不同的结果。 使用 DP：
1. {P,~S}
6. {Q} from 1 and 2
2. {~P,R}
3'. {P,S}
4'. {~P,~S}
7. {P} from 3' and 5
2. {R}
4'. {~R}
8. {}
所以不满意。但是使用 dplL：
1. {P,~S}
6. {P} split(P)
2'. {R}
4'. {Q,~R}
7.{Q}
这意味着它是可满足的...我做错了什么？
解决方法
在DP中的第一次推理中，解析规则没有正确应用。让我们关注从 6. {Q} from 1 and 2 和 1. {P,Q,~R} 推断 2. {P,~R}。将 P、Q 和 R 赋值给 false 满足 {P,~R} 和 {~P,R}，但它不满足推理所声称的 {Q} 由前两个包含。 {P,R} 的可能解析为：
-
{Q,~R,R}通过解析P -
{P,~P}通过解析R
这两个子句始终为真，并被 DP 丢弃。 （丢弃有时称为重言式规则。）这些不包含 {Q}，如前面的反例所示。
另请注意，在 DPLL 示例中，您已将 P、R、Q 指定为 true。这与子句 4. {~P,~Q,~R} 不一致。对于这种分裂，需要彻底应用单元传播。