satisfiability - CNF 与喇叭可满足性

Question

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

Answer 1

喇叭可满足性的存在或不存在可以以线性时间显示。这是一个很好的介绍和一些例子。可以通过单元传播找到解决方案，无需回溯。

加州大学伯克利分校 讲义中的伪代码：

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