Bornes Inférieures et Séparations pour la Compilation de Connaissances Bottom-Up

La compilation de connaissances est un domaine de l’informatique qui étudie les différentes classes de représentations pour les fonctions, et les algorithmes permettant de passer d’une classe à l’autre. Dans cette présentation, on s’intéresse à l’approche de compilation dite bottom-up (ascendante) pour les fonctions Booléennes données comme des formules CNF. Cette approche permet de construire une représentation de la formule – ou de la “compiler” – dans des classes telles que la classe des OBDD (Ordered Binary Decision Diagrams) ou la classe des SDD (Sentential Decision Diagrams). Pour compiler une formule CNF, l’approche bottom-up compile des sous-formules de la CNF et combine les résultats de ces compilations intermédiaires. Il est cependant possible que l’espace nécessaire pour stocker ces résultats intermédiaires soit beaucoup plus grand que l’espace nécessaire pour stocker à la fois la CNF d’entrée et sa représentation en sortie de compilation. Dans ce cas la compilation est jugée inefficace. Nous présentons des bornes inférieures exponentielles pour la compilation bottom-up de formules CNF ayant pourtant des petites représentations dans les classes OBDD ou SDD. Nous décrivons également différentes variantes de compilation bottom-up et comparons leur efficacité.