Problem Detail: 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.
Asked By : John Threepwood
Answered By : Yuval Filmus
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/7473
