文章/答案/技术大牛

发布

社区首页 >问答首页 >DP和DPLL的可满足性产生不同的结果

问DP和DPLL的可满足性产生不同的结果
EN

Stack Overflow用户

提问于 2021-01-23 17:57:20

回答 1查看 35关注 0票数 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}

这意味着它是可以满足的..。我做错什么了？

sat

satisfiability

logic

回答 1

Stack Overflow用户

发布于 2021-01-24 06:14:22

在DP中的第一个推理中，未正确应用解决规则。让我们把重点放在1. {P,Q,~R}和2. {P,Q,~R}对6. {Q} from 1 and 2的推断上。P，Q和R对false的赋值满足{P,Q,~R}和{~P,R}，但它不满足{Q}，而推理声称前两个是需要的。{P,Q,~R}和{~P,R}的可能解决方案包括：

通过解析在P

{P, Q, ~P}上解析
{Q, ~R, R}通过在R

上解析

这两个子句始终为真，并被DP丢弃。(丢弃有时被称为重言式规则。)这些不需要{Q}，如前面的计数器示例所示。

另请注意，在DPLL示例中，您已将P、R、Q指定为true。这与子句4. {~P,~Q,~R}不一致。对于此拆分，需要详尽地应用单元传播。

您可以在网上找到有关DP和DPLL的许多演示文稿。示例：1、2。试着始终如一地详尽地应用规则。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/65857819

复制

相似问题

问DP和DPLL的可满足性产生不同的结果
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DP和DPLL的可满足性产生不同的结果EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问DP和DPLL的可满足性产生不同的结果
EN