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.

  • 5
    Not all constraint solvers use CNF as input. Some prefer not to, because the structure of the original constraint set is preserved. – Dave Clarke Sep 17 '10 at 15:56
  • 1
    this question has a mistaken premise & dont think it deserves such high rating as currently phrased. SAT is defined as the solution of CNF formulas. there is a problem of solving DNFs (you could even call it finding satisfying assignments) but it is not called/nicknamed SAT in CS. & imho this should be migrated to cs.se ... another note-- converting CNF to DNF and vice versa is actually very similar to, or can be seen as, a compression algorithm which fails badly on particular cases (leading to exponential blowup in size) – vzn Oct 22 '12 at 23:24
  • 10
    @vzn: actually, "SAT" is used sometimes to refer to the problem of finding a satisfying assignment for any boolean formula. CNF-SAT is just the most interesting special case, so that we tend to use "SAT" to refer to CNF-SAT in particular as a sort of synechdoche. DNF-SAT, of course, is efficiently solvable, in the same way that CNF-TAUTOLOGY is efficiently solvable. The question does seem to be premised on not realising that. – Niel de Beaudrap Oct 23 '12 at 12:12
up vote 56 down vote accepted

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!

  • afaik the conversion of DNF to CNF and vice versa is not exactly the same as P vs NP although it does probably relate to some important complexity class separations (apparently for classes "larger" than NP)... the issue is it can lead to an exponential blowup in size...and in any case conversion between CNF and DNF is not a decision problem...there are multiple ways to turn it into a decision problem... – vzn Oct 22 '12 at 23:20
  • 10
    I think JeffE's point was that DNF-SAT is in P, so it can't be NP-complete unless P=NP. – Luke Mathieson Oct 23 '12 at 0:11
  • 2
    "all known transformations" is not correct given current knowledge, afaik there are DNF<=>CNF formulas/conversions that provably require exponential space blowup regardless of algorithm...guess it seemed like discussion of CNF<=>DNF conversion was highly relevant to this question & this answer hints at it... is the abbrev "DNF-SAT" used anywhere in the literature? dont recall seeing it myself... it seems inherently confusing to me... DNF-satisfying is a decision problem, DNF<->CNF conversion is a function problem & the answer does not make that distinction too clear; a great answer would... – vzn Oct 23 '12 at 5:14
  • @JɛffE: do you mind clarifying what you meant by "arbitrary boolean formula" here? Looking at Karp's paper, page 92, SATISFIABILITY is defined on CNF formulas. This does not affect your answer to the OP's question, but I am trying to make sure there's no more general results for arbitrary boolean formulas (i.e. formulas that are not necessarily in CNF). Thanks – lyes Oct 25 '15 at 21:03

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.

  • 1
    Good reference: soe.ucsc.edu/classes/cmps132/Winter05/hw/hw8sols.pdf – M.S. Dousti Apr 2 '11 at 22:35
  • 1
    @TayfunPay they do. For example, $\{\{\lnot x\lor x\}\}$. If you disallow clauses containing the same variable twice, then there is a single representation of a tautology, which is the empty set of clauses. – Mikolas Apr 3 '11 at 20:05
  • 3
    @Tayfun while I do agree that definitions typically do disallow repeating variables in clauses, I don't think I have ever seen a definition that would be disallowing the empty set of clauses. (And it is not clear to me why you would want to do that) – Mikolas Apr 3 '11 at 22:20
  • 2
    @Tayfun 1) could you point me to a publication that says that there are no tautologies in CNF or that the empty set of clauses is not CNF? 2) if you disallow the empty set of clauses, then you should also disallow the empty clause and you cannot represent false either 3) if you do not allow true and/or false in CNF, you are losing the property of being able to represent all Boolean functions, why would you want to do that? – Mikolas Apr 4 '11 at 0:41
  • 1
    "there should be no repetition of variables nor literals in any given clause." --- that doesn't disallow empty formulas or clauses. BTW If you disallow the empty clause, you no longer can do resolution refutation proofs, which constitute a fairly important part of automated reasoning. – Mikolas Apr 4 '11 at 11:02

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.

7th 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?

  • 4
    To get the correct LaTeX formatting, replace \and and \or with \land and \lor (or \wedge and \vee). – Jeffε Sep 17 '10 at 15:52
  • 1
    This insight by Giorgio Camerani is not good. The same exponential increase in the number of clauses can happen if you convert something to CNF. Pick this same example and replace "and"s with "or"s. The conversion from this small DNF expression to the CNF will be huge just the same. They have a bit of a ying-and-yang relationship to them. – dividebyzero Oct 22 '12 at 17:46
  • 1
    There is nothing inherently more compact about a transformation to the regular CNF, the real key to the OP question is the fact that you can create those "equisatisfiable" CNF functions with auxiliary variables. There is probably a similar approximation you can do with the DNF to solve a different problem instead of testing for satisfiability. (equi-unsatisfiability functions?...) – dividebyzero Oct 22 '12 at 17:46
  • @dividebyzero: I've devoted a separate answer to address your comments. – Giorgio Camerani Sep 7 '13 at 10:57

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.

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.

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.

  • 1
    What is a "PL formula" and what does "NF" mean? – Joshua Grochow Jun 16 '15 at 19:23
  • 4
    There are a few issues here. (1) I think by "unfalsifiability" you mean "tautology". (2) KNF should be CNF. – Huck Bennett Jun 16 '15 at 19:48
  • 2
    Still not clear what you mean by "NF (retain satisfiability)". Does that mean an algorithm A such that $A(\varphi)$ is satisfiable if $\varphi$ is, but if $\varphi$ is unsatisfiable then $A(\varphi)$ can be either, and furthermore for all satisfiable formulae $\varphi$, $A(\varphi)$ has the same output? That's what I would think from your notation, but this problem wouldn't be in P for CNFs. So what do you mean? – Joshua Grochow Jun 16 '15 at 22:23
  • 1
    (1) "predicate logic" should be "propositional logic". (2) The conversions to normal forms are not decision problems, but function problems (or rather, search problems, as the "normal forms" are not unique). So, the decision classes given in the table are inappropriate. – Emil Jeřábek Jun 17 '15 at 8:08
  • 1
    What is the $\Delta_3^P$ doing there? – Emil Jeřábek Jun 17 '15 at 8:14

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.