algorithm - 使用图的 Horn SAT 算法

Question

对于某些受限类的逻辑公式，可满足性问题可以在多项式时间甚至线性时间内有效地解决。一类是霍恩公式，它仅由霍恩从句组成，最多有一个正面文字。我听说可以使用图表在线性时间内解决 Horn SAT，但找不到此类解决方案的任何实现。现在我真的很感兴趣它是否可能，如果是的话，算法会是什么样子？

Answer 1

如果您熟悉Davis–Putnam–Logemann–Loveland，那么 Horn 子句是一类可以使用一轮单元传播解决的公式，无需回溯。

在图的术语中，我们做了显而易见的事情并建立了一个二分图，其中一侧是变量，另一侧是子句，边表示在子句中显示为否定文字的变量。我们还有一个由单个正文字组成的子句工作队列。当工作队列不为空时，弹出任意元素，识别变量对应的节点，并删除它及其邻居。对于现在度数为零的每个子句顶点，会发生以下两种情况之一。如果该子句具有正字面量，那么我们将其添加到工作队列中。否则，我们已经证明该公式是不可满足的。如果我们到达工作队列的末尾而没有找到这样的子句，那么公式是可满足的，并且一个令人满意的分配是将所有进入工作队列的变量设置为 true，而将所有其他变量设置为 false。