Expander CNFs have Exponential DNNF Size.

Abstract

We prove an unconditional exponential lower bound on the DNNF size of CNF formulas based on a family of expander graphs; thus far, only a superpolynomial lower bound was known, subject to the condition that the polynomial hierarchy does not collapse. As corollaries we obtain that, in general, negating a DNNF leads to an exponential increase in size (this was known to hold if P is not equal to NP), and that the language of prime implicates (PI) can be exponentially more succinct than DNNFs (this was not even known conditionally). These results settle three open problems in the area of knowledge compilation [Adnan Darwiche and Pierre Marquis, A Knowledge Compilation Map, 2002].