Propositional formula in DNF can be decided in polynomial time?

Question

For a given propositional formula f in DNF, one can decide in polynomial time, if the formula is satisfiable: Just walk through all subformulas (l_1 and ... and l_k) and check, wheter it has NO complementary pair of literals. Formula f is satisfiable iff such subformula exists.

Is my approach above correct ?

If yes, I'm wondering why all modern SAT solvers get a CNF as input format, and don't just use DNF.

Answer 1

The conversion from CNF to DNF can come at an exponential cost. For example $(a_1 \lor b_1) \land \cdots \land (a_n \lor b_n)$ expands to $2^n$ many terms. As you comment, for DNF satisfiability is easy - it is falsifiability which is hard. If the problem is trivial, you don't input it to a SAT solver, and that's why SAT solvers accept CNFs instead of DNFs.

If you believe that P is different from NP, then this implies that there is no polynomial time way to convert CNF satisfiability to DNF satisfiability, since the former is NP-complete while the latter is in P.