Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
When hand-manipulating algebra DNF (sum of products) is easier than CNF (product of sums). Possibly because factoring is more difficult than expanding. So why is it the opposite for computational boolean algebra?
Perhaps one argument is that in CNF one can show that an expression is false by showing that one clause is false. But that is no different from showing that an expression is true by showing that one conjunction is true.
One (serious) issue is that converting to DNF is harder than solving the SAT problem itself! E.g. you can see that:
$$ x\wedge y\ \vee\ x\wedge \neg z$$
has 2 solutions, $x=\top,\ y=\top$ and $x=\top,\ z=\bot$, without doing any fancy work.
This means that converting into DNF is going to be tough, as opposed to CNF for which there are efficient algorithms. Note that in the CNF conversion, the result is not strictly equivalent but merely equisatisfiable, which is all that SAT solvers care about.
