# 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, 2019 at 16:15
• I found one implementation of this method in this Repo github.com/netom/satispy Sep 2, 2019 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, 2019 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, 2019 at 12:15

## 2 Answers

Any algorithm necessarily has exponential complexity, since the CNF of a formula can be exponentially longer than the DNF, and the input might be in DNF.

If you require a logically equivalent CNF formula, then that will give you a worst-case exponential size formula.

If, however, equisatisfiability is enough, then you can use Tseitin encoding, which will give you a polynomial size formula. The trick is in adding new atoms for logical operators.