將任何命題公式轉換爲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。