• HDR soutenu le :
  • 15 juin 2026 • Salle des thèses, faculté des sciences

Résumé

Ce manuscrit est un résumé de mes recherches ces dix dernières années. Il s’intéresse à la manière dont les structures de données issues de la compilation des connaissances, traditionnellement centrées sur la logique propositionnelle et l’IA, peuvent être appliquées à d’autres domaines de l’informatique. Nous commencer par introduire les principales structures de données et notions utilisées en compilation des connaissances. Nous présentons ensuite une nouvelle structure de données permettant de représenter les fonctions Booléennes qui peut être vue comme une généralisation canoniques des OBDD à des ordres arborescents. Elle permet de retrouver de nombreux résultats de façon unifiée.

Nous nous intéressons ensuite à l’utilisation de telles structures de données pour certifier les solveurs #SAT. Nous montrons comment les modifier pour qu’ils produisent un certificat permettant de vérifier indépendamment que la formule d’entrée possède en effet le nombre de modèles indiqués par le solveur.

Nous étudions ensuite des généralisations de ces structures de données aux domaines non binaires et montrons comment les utiliser pour représenter et analyser les réponses d’une requête de base de données.

Enfin, nous exhibons un lien entre la compilation de connaissances et la notion de formulations étendues, dont le but est de décrire un polyèdre avec peu de contraintes linéaires, en utilisant éventuellement un espace de dimension plus grand. Nous montrons qu’on peut extraire une formulation étendue de taille linéaire d’un circuit DNNF décrivant l’enveloppe convexe de ses modèles, vu comme des points dans {0,1}^n. Nous appliquons ce résultat au problème d’optimisation polynomiale binaire et prouvons de nouveaux résultats de tractabilité.

Composition du jury

Garant

  • Pierre Marquis, Professeur, Université d’Artois

Rapporteurs

  • Gilles Audemard, Université d’Artois
  • Olaf Beyersdorff, Friedrich Schiller University Jena
  • Hubie Chen, King’s College London

Examinateurs

  • Luce Brotcorne, Inria Lille
  • Bruno Zanuttini, Université de Caen