# Propositional formula in DNF can be decided in polynomial time?

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.

-

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.

-
Thank you. I was just wondering: When the SAT problem for DNF formulas is in P, why not just describe problems directly into DNF (instead of CNF) ? Because translating a formula into CNF might take exponential cost as well as translating it into DNF. – John Threepwood Dec 17 '12 at 22:26
@JohnThreepwood most problems aren't easily expressed in DNF. And, the conversions to DNF usually take exponential time, and necessarily so, for example if there are exponential satisfiable solutions. – Realz Slaw Dec 18 '12 at 2:57
@RealzSlaw Thank you. So most real-life problems are easier encoded in CNF. Is this because most problems are 'naturally' structured as constraints (in CNF each clause is a constraint) ? – John Threepwood Dec 18 '12 at 16:10
@JohnThreepwood If a problem can be expressed as DNF, a satisfiable assignment is there naturally. There would be nothing to solve. And intuitively yes, I think the problems solved using SAT solvers are naturally described via constraints which CNF is useful for. – Realz Slaw Dec 18 '12 at 17:29
@RealzSlaw Good point. That helped understanding. – John Threepwood Dec 18 '12 at 18:05