Conjunctive vs. Disjunctive Normal Form

[Van-Hau Nguyen]

Dear everyone,

It is well-known that:

 There is an algorithm which transforms any propositional formula into a semantically equivalent formula in conjunctive normal form - CNF (or disjunctive normal form - DNF).

And it is obvious that testing DNF being satisfiable is trivial. This leads to a very interesting question of why almost, if not all SAT solvers use CNF instead of DNF?

Could you please give me any help?

Thank you.

​Cheers,​

--

Van-Hau Nguyen

[Hadi Katebi]

DNF can grow exponentially large.

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Meenal Chougule]

CNF too.. So how they are compared?and concluded that CNF is better to solve than DNF. Solving DNF parallely is much easier than CNF

--
Meenal D Chougule

[Hadi Katebi]

There exists a conversion for any formula to a CNF formula such that the satisfiability (not the equivalence!) of the formula is preserved and yet the size of the CNF formula is increased non-exponentially (in fact, linearly). No such conversion is known for DNF, so DNF can grow exponentially large.