# Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?

I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:

1. elimination of equivalence
2. Elimination of Implications
3. elimination of double negation
4. De Morgan Laws
5. distributive law

I found one implementation of this method in this Repo https://github.com/netom/satispy

Thanks

• Can you summarize the algorithm in the question, to make your question self-contained, so we don't have to read external links or read a book to understand the question? What are your thoughts? Are there any steps where you do know what the complexity will be? – D.W. Sep 2 '19 at 16:15
• I found one implementation of this method in this Repo github.com/netom/satispy – dimitruss Sep 2 '19 at 16:29
• Sorry, that's still an external link, so it doesn't address my comment. Trying to read someone else's code that implements an algorithm is often a miserable way to understand what the algorithm is doing. – D.W. Sep 2 '19 at 16:31
• I would think that this question is answered in sufficient depth in Sisper's book, assuming you can relate your textbook algorithm to what's discussed in Sipser's book. The two answers given so far show exactly where the difference is: weakening the requirements for the conversion algorithm from equivalence to equisatisfiability is a sufficient step to overcome the otherwise exponential hardness of the problem. – Kai Oct 15 '19 at 12:15