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:


elimination of equivalence
Elimination of Implications
elimination of double negation
De Morgan Laws
distributive law


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

Thanks
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.