Séminaire MAGMAT, Vendredi 13 février

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.


DMC Firewall is developed by Dean Marshall Consultancy Ltd