CNF与Horn可满足性(CNF vs Horn Satisfiability)

CNF与Horn可满足性(CNF vs Horn Satisfiability)

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

I know that it's easier to prove if a horn-formula is satisfiable. My Question is: Why is it easier with a horn formula rather than a normal CNF?

最满意答案

可以在线性时间内显示Horn可满足性的存在或不存在。 以下是一些很好的介绍。 可以通过单元传播找到解决方案而无需回溯。

伯克利大学的伪代码讲义 ：

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

Presence or absence of Horn satisfiability can be shown in linear time. Here is a good introduction with some examples. The solution can be found by unit propagation without backtracking.

Pseudocode from a UC Berkeley lecture note:

Satisfiability for general CNF expressions is a classic NP-complete problem. No polynomial time algorithms are known for CNF satisfiability (except if P=NP).