将任何命题公式转换为CNF格式的复杂性

Question

将任何命题公式转换为CNF格式的复杂程度如何？这是一个NP完全问题吗？

Answer 1

标准算法的通用格式良好的公式转变成相当于 CNF有指数运行时间，因为in the worst case a n-clauses WFF is equivalento to a 2^n-clauses CNF。

但是，您可以在多项式时间任意布尔公式为CNF是不stricty相当，但satisfable只有在布尔公式是satisfable变换。这是用于证明3CNF是NP完全的标准缩减，给出了更一般的SAT是NP完全的。请参阅here。