Florent Capelli (IMJ, Paris Diderot)

Le problème #SAT, qui consiste à compter le nombre de solutions d’une formule donnée sous forme normale conjonctive (CNF), est connu pour être difficile tant à résoudre qu’à approximer. Afin de résoudre en pratique ce problème, il est intéressant de comprendre comment on peut tirer profit de la structure de l’entrée pour obtenir des algorithmes en temps polynomial pour certaines instances.

Une méthode qui a fait ses preuves consiste à associer un graphe ou un hypergraphe à une formule CNF et à regarder l’influence de certaines mesures de graphes classiques (treewidth, clique-width, acyclicité d’hypergraphe…) sur la complexité du problème.

Dans cette présentation, nous essaierons de donner un aperçu général des différentes mesures de graphe que l’on peut exploiter efficacement pour ce problème et nous détaillerons en particulier l’influence des différentes notions d’acyclicité d’hypergraphe pour ce problème.