5
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – John Threepwood
    Dec 17, 2012 at 22:26
  • 1
    $\begingroup$ @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. $\endgroup$
    – Realz Slaw
    Dec 18, 2012 at 2:57
  • $\begingroup$ @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) ? $\endgroup$
    – John Threepwood
    Dec 18, 2012 at 16:10
  • 1
    $\begingroup$ @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. $\endgroup$
    – Realz Slaw
    Dec 18, 2012 at 17:29
  • $\begingroup$ @RealzSlaw Good point. That helped understanding. $\endgroup$
    – John Threepwood
    Dec 18, 2012 at 18:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.