Complexité de conversion d'une formule propositionnelle au format CNF

Question

Quelle est la complexité de la conversion d'une formule propositionnelle au format CNF? Est-ce un problème NP-complet?

Answer 1

L'algorithme standard pour transformer une formule générale bien formés à un équivalent CNF a un temps d'exécution exponentielle , depuis in the worst case a n-clauses WFF is equivalento to a 2^n-clauses CNF.

Cependant, vous pouvez transformer en temps polynomial une formule booléenne arbitraire dans un CNF qui est pas stricty équivalent, mais satisfable que si la formule booléenne est satisfable. C'est la réduction standard utilisée pour prouver que 3CNF est NP-complet, à condition que le SAT plus général soit NP-complet. Voir here.