Why is CNF used for SAT and not DNF?

Question

I don't quite understand why almost all SAT solvers use CNF instead of DNF. It seems to me that solving SAT is easier using DNF. After all, you just have to scan through the set of implicants and check whether one of them contains not both a variable and its negation. For CNF, there's no simple procedure like this.

Answer 1

The textbook reduction from SAT to 3SAT, due to Karp, transforms an arbitrary boolean formula $\Phi$ into an “equivalent” CNF boolean formula $\Phi'$ of polynomial size, such that $\Phi$ is satisfiable if and only if $\Phi'$ is satisfiable. (Strictly speaking, these two formulas are not equivalent, because $\Phi'$ has additional variables, but the value of $\Phi'$ doesn't actually depend on those new variables.)

No similar reduction from arbitrary boolean formulas into DNF formulas is known; all known transformations increase the size of the formula exponentially. Moreover, unless P=NP, no such reduction is possible!

Answer 2

Most of the important things were said but I would like to stress a few points.

1. satisfiability of a DNF formula is P
2. satisfiability of a CNF formula is NP
3. testing if a CNF formula is a tautology is P
4. testing if a DNF formula is a tautology is coNP
5. negating DNF yields CNF and vice versa

So SAT solvers use CNF because they target satisfiability and any formula can be translated to a CNF while preserving satisfiability in linear time.

Answer 3

SAT solvers don't "use" CNF -- they are (often) given CNF as inputs and do their best to solve the CNF they are given. As your question points out, representation is everything -- it is much easier to tell whether a DNF is satisfiable than a CNF of the same size.

This leads to the question of why SAT solvers can't just turn their given CNF into a DNF and solve the resulting DNF, and trying this is a good exercise to go through in understanding issues of representation.

Answer 4

7^th September 2013: Further answer added, check bottom of page

---

Basically, a DNF formula is a disjunction of clauses $c_1 \lor ... \lor c_m$, where each clause $c_i = l_{i,1} \land ... \land l_{i,k}$ is a conjuction of literals. Let's call a clause $c_i$ conflicting if and only if it contains both a literal $l$ and its negation $\lnot l$. It's easy to see that each non-conflicting clause just encodes $2^{n-k}$ solutions of the formula. So the whole DNF is just an enumeration of solutions. A formula may have exponentially many solutions, so the corresponding DNF formula may have exponentially many clauses. Try to convert this CNF formula:

$l_1 \lor l_2 \lor l_3 \lor l_4$

$l_5 \lor l_6 \lor l_7 \lor l_8$

$l_9 \lor l_{10} \lor l_{11} \lor l_{12}$

$l_{13} \lor l_{14} \lor l_{15} \lor l_{16}$

$l_{17} \lor l_{18} \lor l_{19} \lor l_{20}$

to its corresponding DNF formula: you'll get too many clauses. In one word: CNF is compact, while DNF is not; CNF is implicit, while DNF is explicit.

The following problem is NP-complete: given a DNF instance, is there an assignment of variables that falsifies all the clauses?

Answer 5

I just realized one more thing, which hopefully deserves a separate answer. The presumption of the question is not entirely true. A binary decision diagram (BDD) could be seen as a compact/refined representation of DNF. There have been some SAT solvers using BDDs but I believe they no longer appear.

There is a nice paper by Darwiche and Marquis studying different properties of various representations of Boolean functions.

Answer 6

This further answer is meant as a feedback to dividebyzero's comment to my previous answer.

As dividebyzero says, it is certainly true that CNF and DNF are two sides of the same coin.

When you have to find a satisfying assignment, DNF is explicit as it manifestedly shows you its satisfying assignments (DNF Satisfiability belongs to $\mathbf{P}$), whereas CNF is implicit as it wraps and winds to hide its satisfying assignments from your eyes (CNF Satisfiability is $\mathbf{NP-complete}$). We do not know any procedure which is able to unwrap and unwind any CNF formula into some equisatisfiable DNF formula which is not exponentially sized. This was the point of my previous answer (whose example was meant to show the exponential blow-up, although admittedly such example was not the best possible choice).

Conversely, when you have to find a falsifying assignment, CNF is explicit as it manifestedly shows you its falsifying assignments (CNF Falsifiability belongs to $\mathbf{P}$), whereas DNF is implicit as it wraps and winds to hide its falsifying assignments from your eyes (DNF Falsifiability is $\mathbf{NP-complete}$). We do not know any procedure which is able to unwrap and unwind any DNF formula into some equifalsifiable CNF formula which is not exponentially sized.

At one extremity we have Contradictions, i.e. unsatisfiable formulas. At the opposite extremity we have Tautologies, i.e. unfalsifiable formulas. In the middle, we have formulas which are both satisfiable and falsifiable.

In any CNF formula with $n$ variables, every clause of length $k$ manifestedly encodes $2^{n-k}$ falsifying assignments.

In any DNF formula with $n$ variables, every term of length $k$ manifestedly encodes $2^{n-k}$ satisfying assignments.

A CNF formula without clauses is a Tautology, because it does not have any falsifying assignment. A CNF formula containing the empty clause (which subsumes every other clause) is a Contradiction, because the empty clause (which has $k = 0$) indicates that all the $2^n$ assignments are falsifying. Any other CNF formula is either a Contradiction or one of those formulas in the middle (and it is $\mathbf{NP-complete}$ to distinguish between these 2 cases).

A DNF formula without terms is a Contradiction, because it does not have any satisfying assignment. A DNF formula containing the empty term (which subsumes every other term) is a Tautology, because the empty term (which has $k = 0$) indicates that all the $2^n$ assignments are satisfying. Any other DNF formula is either a Tautology or one of those formulas in the middle (and it is $\mathbf{NP-complete}$ to distinguish between these 2 cases).

With a CNF formula, distinguishing between the 2 cases above means being able to tell whether all the falsifying assignments collectively brought by the presence of clauses overlap in such a way to cover all the $2^n$ assignments (in which case the formula is a Contradiction, otherwise it is satisfiable).

With a DNF formula, distinguishing between the 2 cases above means being able to tell whether all the satisfying assignments collectively brought by the presence of terms overlap in such a way to cover all the $2^n$ assignments (in which case the formula is a Tautology, otherwise it is falsifiable).

Under this light it becomes more clear why CNF Satisfiability and DNF Falsifiability are equivalent in terms of computational hardness. Because they actually are the very same problem, as the underlying task is exactly the same: to tell whether the union of several sets equals the space of all possibilities. Such task leads us to the wider realm of counting, which is in my humble opinion one of those avenues to be fervently explored in order to hope to make some non-negligible progress on these problems (I doubt that further research on resolution-based solvers may eventually bring groundbreaking theoretical advancements, while it certainly continues to bring surprising practical advancements).

The difficulty of such task is that those sets overlap wildly, in an inclusion - exclusion fashion.

The presence of such overlapping is precisely where the hardness of counting resides. Moreover, the fact that we let those sets overlap is the very reason that allows us to have compact formulas whose solution space is nevertheless exponentially large.

Answer 7

I've decided to turn all these answers in this thread (especially Giorgio Camerani’s answer) into a nice table so that the duality is visible at a single glance:

\begin{array} {r|c|c} &\text{DNF} & \text{CNF} \\\hline \text{tautology/unfalsifiability} & \textsf{coNP-complete} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} \\\hline \text{satisfiability} & \textsf{P} \; \tiny\text{(sat. assignments are explicit)} & \textsf{NP-complete}\\\hline \text{falsifiability} & \textsf{NP-complete} & \textsf{P} \; \tiny\text{(fals. assignments are explicit)} \\\hline \text{unsatisfiability} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} & \textsf{coNP-complete} \\\hline \tiny{\text{conversion to normal form, retaining equivalence}} & (*) & (*) \\\hline \tiny{\text{conversion to normal form, retaining satisfiability}} & (**) & \textsf{FP} \\\hline \tiny{\text{conversion to normal form, retaining falsiability}} & \textsf{FP} & (**) \end{array}

$(*)$: These search problems, as well as DNF to CNF conversion (or vice versa for that matter), require exponential time due to the sheer size of the output. They are in FPSPACE; in fact, they are solvable by a function with a polynomial-time bit-graph, which is as efficient as it gets for an exponential-size-output function, but I’m not aware of this class having a name. Usual notions of poly-time reductions only work sensibly for functions with polynomial-size output; applying them blindly to the present case would make all these search problems FEXP-complete, again due to the size of the output.

$(**)$: These search problems are solvable by an exponential-time function with a polynomial-time bit-graph as in $(*)$. However, they are also solvable in $\mathrm{FP}^{\mathrm{NP}[1]}$, and conversely, they are NP-hard under poly-time Turing reductions (many-one reductions make no sense here, as we are comparing a search problem with a decision problem).

Shortest answer to the question: showing satisfiability (solving SAT) via DNF can only be done in exponential time according to the table above.