What's the most efficient way to convert any propositionnal logic formula to DNF

Question

In every paper that I've read so far, authors say that they convert a formula into disjunctive normal form (DNF) but they don't give any detail on how they are doing it.

The only way of converting a formula $F$ into an equivalent formula $G$ in DNF ($F \equiv G$) that I know is by converting it in negation normal form and then into DNF by distributing conjunctions over disjunctions. I know that using this method, the size of $G$ may be exponential in the size of $F$ so I was wondering if there is a more efficient way of doing this ?

Answer 1

Well, I think there is no shortcut because of the satisfiability problem which is NP-complete.

What you can do to expand an expression to DNF is to multiply out first using the law of distributivity. And then if you have a term like $xy$ and there is a third variable $z$, then replace $xy$ by $xy(z+\bar z) = xyz + xy\bar z$. Hope it helps.

Answer 2

I know that using this method, the size of $G$ may be exponential in the size of $F$

That is not a failing of the method -- it is inherent in the problem that a DNF may need to be exponentially large.

More precisely, we can construct a family of $F_n$s of size linear in $n$ such that every DNF that is equivalent to $F_n$ must have at least $2^n$ clauses.

Namely first let the formula $P(a,b,c)$ have the truth value of "$c$ is the exclusive OR of $a$ and $b$". I won't get into the boring details of how to do that, but clearly there is some fixed, finite formula that has this property. Now let $$ F_n(x_1,\ldots,x_n,y_1,\ldots,y_n) \equiv (x_1\leftrightarrow y_1) \land P(y_1,x_2,y_2) \land P(y_2,x_3,y_3) \land \cdots \land P(y_{n-1},x_n,y_n) \land y_n $$

Then $F_n$ is true exactly if an odd number of the $x_i$s are true, and additionally the $y_i$ have certain particular truth values that we can compute from the $x_i$s. Each of those $2^{n-1}$ cases must be covered by some clause in the DNF -- and that clause must necessarily contain a literal for each of the $x_i$s, because otherwise we could flip that $x_i$ that doesn't have one and get something the DNF certainly shouldn't be true for. So the clause can't be true for any other truth assignment that satisfies $F_n$ -- in other words each of the $2^{n-1}$ satisfying inputs needs its own clause.