CNF 与喇叭可满足性

Question

我知道证明一个角公式是否可满足更容易。我的问题是：为什么使用喇叭公式而不是普通 CNF 更容易？

Answer 1

Horn satisfiability 的存在与否可以以线性时间显示。 Here 是一个很好的介绍，并带有一些示例。无需回溯，unit propagation即可找到解决方案。

来自 UC Berkeley 的伪代码 lecture note:

一般 CNF 表达式的可满足性是一个经典的NP-complete 问题。对于 CNF 可满足性，没有已知的多项式时间算法（除非 P=NP）。