Expander CNFs have Exponential DNNF Size
Stefan Mengel22 janv. 2015 - 14:00
DNNFs are a class of Boolean circuits studied in the area of knowledge compilation where they serve as a target language into which knowledge bases are compiled. DNNFs form a very general language; in particular they generalize classical languages like OBDDs and DNF-formulas. While it was known that under standard complexity theoretic assumptions CNF formulas can generally not be compiled into DNNFs without a superpolynomial size blow-up, no concrete, unconditional lower bounds were known for DNNFs. In joint work with Simone Bova, Florent Capelli and Friedrich Slivovsky, we showed such a lower bound, proving that there are CNF-formulas of size linear in the number of variables that cannot be compiled into DNNFs of subexponential size. In this talk I will explain our result, describe the hard CNF formulas and sketch some of the key parts of the proof.