Ce vendredi nous accueillerons Stefan Mengel du Lix.

L'exposé aura lieu en salle 301 à 10h30. Venez tout apprendre des SAT solver modernes et de langages de représentations de formules DNF/CNF,

le tout matiné de graphs expander.

### Expander CNFs have Exponential DNNF Size

DNNFs are a class of Boolean circuits studied in the area of knowledge compilation in artificial intelligence where they serve as a target language into which knowledge bases are compiled. DNNFs form a very general language; in articular 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 give and introduction into the area, explain our result, describe the hard CNF formulas and sketch some of the key parts of the proof.