Solving SAT by converting to disjunctive normal form

The first well-known $NPC$ problem is the Boolean Satisfiability Problem, which has a proof of being $NPC$ done by Cook (Cook-Levin Theorem).

The problem can easily be described the following way:

In complexity theory, the satisfiability problem (SAT) is a decision problem, whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses. So, we should give an answer ‘yes’ if there is a set of boolean variables which yield ‘TRUE’ for the given for the corresponding expression.

However, I have a question. The wikipedia article states the following:

SAT is easier if the formulas are restricted to those in disjunctive normal form, that is, they are disjunction (OR) of terms, where each term is a conjunction (AND) of literals (possibly negated variables). Such a formula is indeed satisfiable if and only if at least one of its terms is satisfiable, and a term is satisfiable if and only if it does not contain both x and NOT x for some variable x. This can be checked in polynomial time.

So, basically, if the expression is written in the DNF, this problem is not $NPC$, but simply $P$.

However, as far as I know, there is a $O(p(n))$ algorithm to transform any given boolean expression into DNF and DNF exists for any boolean expression.

What am I missing or misinterpreting? There is obviously an error in my logic, because it resulted in making the SAT problem $P$, but not $NP$.

Thank you!

Solutions Collecting From Web of "Solving SAT by converting to disjunctive normal form"

Your claim that you can convert an arbitrary formula to DNF in polynomial time is mistaken.

You can convert a boolean formula into DNF, but the resulting formula might be very much larger than the original formula—in fact, exponentially so. Since the conversion algorithm must at the very least write out the resulting DNF formula, its running time must be at least the length of the output, and therefore its worst-case running time must be exponential.

Even if you somehow finesse the issue of writing out the DNF version of the input formula, the algorithm you propose takes a formula of size $x$, converts it into a DNF formula of worst-case size $2^x$, and then calculates satisfiability of the DNF formula in time $P(2^x)$ for some polynomial $P$. This is no better in general than just trying every possible satisfying assignment in the original formula.

The Wikipedia article on “Disjunctive Normal Form” has an example of a formula that explodes when converted to DNF. But it’s an easy example. Consider:

$$(A_1\lor B_1)\land(A_2\lor B_2)\land\cdots\land(A_n\lor B_n)$$

This has length proportional to $n$. But in DNF it turns into:

$$(A_1\land A_2\land\cdots\land A_n)\lor\\
(B_1\land A_2\land\cdots\land A_n) \lor \\
(A_1\land B_2\land\cdots\land A_n) \lor \\
(B_1\land B_2\land\cdots\land A_n) \lor \\
(B_1\land B_2\land\cdots\land B_n)\hphantom{\lor}

with $2^n$ clauses.