对于一些受限制的逻辑公式类别，可满足性问题可以在多项式时间甚至线性时间内高效地解决。其中之一是Horn公式类别，它只由至多一个正文字的Horn子句构成。我听说可以使用图形以线性时间解决Horn SAT问题，但找不到这种解决方案的任何实现。现在我非常想知道是否可能，并且如果可能，算法会是什么样子？
1个回答
3
如果您熟悉Davis–Putnam–Logemann–Loveland，那么Horn子句是一类可以使用一轮单元传播解决的公式，无需回溯。在图形术语中，我们可以将变量放在一侧，子句放在另一侧，边表示变量在子句中出现为否定文字。我们还有一个由单个正文字组成的子句工作队列。只要工作队列不为空，就弹出任何元素，找到对应变量的节点并删除它及其邻居。对于现在度数为零的每个子句顶点，会发生以下两种情况之一。如果该子句具有正文字，则将其添加到工作队列中。否则，我们已经证明了该公式是不可满足的。如果我们在没有找到这样的子句的情况下到达工作队列的末尾，则该公式是可满足的，并且一种满足的赋值方式是将所有进入工作队列的变量设置为true，将其他变量设置为false。
- David Eisenstat
3
听起来很清晰和合乎逻辑，但问题在于这里。假设我们有以下公式：(w ∧ y ∧ z ⇒ x) ∧ (x ∧ z ⇒ w) ∧ (x ⇒ y) ∧ (⇒ x) ∧ (x ∧ y ⇒ w) ∧ (!w ∨ !x ∨ !y) ∧ !z（'!'表示否定）。它是不可满足的，算法将确认这一点。为了使其可满足，我们可以做一个小改变：(w ∧ y ∧ z ⇒ x) ∧ (x ∧ z ⇒ w) ∧ (x ⇒ y) ∧ (⇒ x) ∧ (x ∧ y ⇒ w) ∧ (!w ∨ !x ∨ !y ∨ !z)。然而，在这种情况下，算法将失败并将其判定为不可满足（解为：w = true，y = true，x = true，z = false）。 - undefined
@Meta 我不明白。在不可满足的例子中，我们从 (⇒ x) 推导出 x，然后从 (x ⇒ y) 推导出 y，因为传播 x 简化了它变成了 (⇒ y)，然后从 (x ∧ y ⇒ w) 推导出 w，这使得 (!w ∨ !x ∨ !y) 变为空。在可满足的例子中，(!w ∨ !x ∨ !y ∨ !z) 仍然有 !z，所以我们以该满足赋值终止。 - undefined
抱歉，我刚才有点迷糊，但现在我真正明白了。非常感谢！ - undefined
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接