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.