Yanis Sellami (avec Mnacho Echenim) : Dénombrement de modèles en logique équationnelle

De Ensiwiki
Aller à : navigation, rechercher
Cornues.png
Titre du projet Dénombrement de modèles en logique équationnelle
Cadre IRL

Labo LIG
Équipe CAPP
Encadrants Mnacho Echenim et Nicolas Peltier


Introduction

On s'intéresse dans ce travail au problème de comptage du nombre d'interprétations validant une formule donnée. En logique propositionnelle, ce problème est noté #SAT. Il consiste à compter, pour une formule F donnée, le nombre d'affectations des variables propositionnelles de F telles que F soit évaluée à vrai. Notre objectif est de traiter le cas où la formule F est interprétée modulo une théorie. On considère uniquement la théorie définie par les axiomes de reflexivité, symétrie et transitivité. Les atomes sont alors des équations de la forme \mathcal{R}(a,b)a,b sont des constantes et \mathcal{R} représente une relation d'équivalence. On se limite de plus au cas où les formules sont des conjonctions de littéraux (atomes ou négations d'un atome).

On cherche ainsi à déterminer une méthode pour effectuer ce comptage, à écrire le code d'un prototype, puis à chercher différentes méthodes pour améliorer l'efficacité dudit prototype.

Problème et comptage de coloriages

Réduction du problème à un problème de comptage de coloriages d'un graphe

Ce problème peut être traité dans un cadre plus général que celui de la logique. On considère ainsi des ensembles quelconques munis de relations d'équivalence partielles définies par un couple \mathcal{R}=(\mathcal{R}^+,\mathcal{R}^-) avec \mathcal{R}^+ une relation d'équivalence où \mathcal{R}^+ représente les éléments qui doivent être en relation par \mathcal{R} et \mathcal{R}^- ceux qui ne doivent pas être en relation par \mathcal{R}. Les autres éléments peuvent ou peuvent ne pas être en relation par \mathcal{R}. Dans ce cadre, on cherche donc à compter le nombre de relations d'équivalence totales (i.e. vérifiant \mathcal{R}^+ \cup \mathcal{R}^- = L^2 et \mathcal{R}^+ \cap \mathcal{R}^- = \varnothing) qui contiennent \mathcal{R}.

Pour faire cela, on construit le graphe associé à la relation partielle. Ce graphe a pour sommets l'ensemble des classes d'équivalences de \mathcal{R}^+ et pour arêtes l'ensemble des relations de \mathcal{R}^-. On a alors que \mathcal{R}' est une relation d'équivalence contenant \mathcal{R} si et seulement s'il existe un coloriage correct du graphe associé à \mathcal{R} pour lequel deux éléments sont en relation par \mathcal{R}' si et seulement s'ils sont dans des classes de \mathcal{R} de même couleur. Ce théorème permet de conclure que l'on peut compter le nombre de relations totales contenant \mathcal{R} en comptant le nombre de coloriages corrects non-équivalents du graphe associé.

Comptage des coloriages corrects et non-équivalents d'un graphe

Pour compter le nombre de coloriages corrects non-équivalents \mathcal{P}(G) d'un graphe, on utilise une méthode décrite dans [1]. Celle-ci donne trois formules pour calculer ce nombre de manière récursive :

Si u et v sont deux sommets du graphe G qui ne sont pas reliés par une arête, on a :

\mathcal{P}(G) = \mathcal{P}(G + uv) + \mathcal{P}(G\setminus uv) (1)

G + uv est le graphe G auquel on a ajouté l'arête (u,v) et \mathcal{P}(G\setminus uv) le graphe G dans lequel on a fusionné les sommets u et v (on les remplace par un autre sommet relié à tous les sommets qui avaient une arête commune soit avec u soit avec v).

De même, si u et v sont reliés par une arête, on a :

\mathcal{P}(G) = \mathcal{P}(G - uv) - \mathcal{P}(G\setminus uv) (2)

G - uv est le graphe G auquel on a retiré l'arête (u,v).

Enfin, si u est un sommet dominant dans G (c'est-à-dire un sommet relié à tous les autres sommets), on a

\mathcal{P}(G) = \mathcal{P}(G-u) (3)

où G-u est le graphe G auquel on retiré le sommet u et toutes les arêtes qui y étaient reliées.

Ces trois relations donnent un algorithme récursif pour calculer le nombre de coloriages corrects non-équivalents d'un graphe, algorithme que l'on va chercher à implanter.

Prototype

Algorithme général

L'algorithme principal consiste à appliquer récursivement les formules énoncées afin de calculer le nombre de coloriages recherché. Cela nécessite en particulier la mise en place de structures de données efficaces pour réaliser les opérations nécessaires sur les graphes.

Représentation schématique de l'algorithme

Structures de données

Pour réaliser l'opération de fusion de manière efficace, on met au point une structure de graphe en place avec une représentation par matrice d'adjacence. Pour réaliser la fusion de deux sommet, on ne parcourt alors qu'une seule fois les sommets du graphe :

Exemple de graphe et de sa représentation par matrice d'adjacence.

on commence par choisir le sommet qui représentera le sommet fusionné. On parcourt ensuite les arêtes reliées à l'autre sommet et on les ajoute au premier. En même temps, on stocke les arêtes ajoutées et les arêtes qui étaient communes aux deux sommets. On signale enfin que l'un des sommets ne fait plus partie du graphe (bien qu'il soit toujours dans la structure). Cela permet de réaliser la fusion de sommets en \Theta(nombre\ de\ sommets). De plus, la sauvegarde des arêtes ajoutées et communes aux deux sommets permet de restaurer le graphe de départ sans parcourir les sommets (juste en parcourant la liste des arêtes ajoutées). On a donc une restauration des sommets fusionnés en O(nombre\ de\ sommets).

Exemple de fusion de nœuds

Pour choisir quelle relation on doit appliquer à partir d'un graphe donné, il a également été nécessaire de mettre en place une structure permettant de conserver efficacement et tout au long des opérations le degré de chaque sommet du graphe (voir partie Mesures).

Mémoisation

Par la suite, on a cherché à appliquer une mémoisation sur les graphes. En effet, comme on compte les coloriages des graphes, on peut se contenter de conserver la valeur pour un représentant d'une classe d'isomorphisme, deux graphes isomorphes ayant le même nombre de coloriages. Pour calculer un représentant canonique de la classe d'isomorphisme d'un graphe, on utilise l'utilitaire nauty ([2]). Il suffit alors de conserver les associations représentant canonique/nombre de coloriages.

Cette fonctionnalité n'a toutefois pas été achevée.

Mesures

On s'intéresse ensuite à observer l'efficacité de l'application des différentes relations sur de graphes. Dans l'ensemble des cas, le prototype conserve une complexité exponentielle.

Le travail a consisté à comparer l'application des relations (1) et (2), sachant que la première est plus efficace pour des graphes contenant beaucoup d'arêtes et la deuxième pour des graphes en contenant peu. On a donc dû déterminer le seuil (nombre d'arêtes du graphe) au niveau duquel on devait changer de formule pour optimiser l'efficacité.

Comparaison du temps d'exécution moyen de l'algorithme suivant qu'on applique la formule (1) (en bleu) ou la formule (2) (en vert) en fonction du nombre d'arêtes pour des graphes de 8 sommets.

On a ensuite ajouté l'application de la troisième formule, le maintien des degrés des sommets dans la structure de graphe permettant de choisir le sommet auquel il est le plus avantageux d'ajouter des arêtes. Cette méthode permet de lisser la courbe du temps moyen d'exécution de manière importante. En effet, il est plus rapide de réduire au maximum le nombre de sommets du graphe avant de se diriger vers l'un des cas de base de l'algorithme.

Comparaison du temps d'exécution moyen de l'algorithme suivant qu'on applique les formules (1) et (2) avec (en bleu) ou sans (en vert) la formule (3) en fonction du nombre d'arêtes pour des graphes de 8 sommets.

Conclusions

Finalement, on est parvenu à mettre au point une méthode pour compter le nombre de relations d'équivalences totales contenant une relation partielle à partir d'une méthode de comptage de coloriages dans un graphe. On a ensuite implanté un prototype qui permet de résoudre le problème pour de petit graphes. La complétion de la mémoisation ou l'utilisation d'autres méthodes plus avancées (graphes cordaux et polynômes chromatiques notamment) devraient pouvoir permettre d'améliorer considérablement l'efficacité du prototype et de l'utiliser sur des graphe de taille plus grande.

Rapport

Fichier:Irl sellamiy.pdf

Références

[1] Hertz et Mélot. « Counting the number of non-equivalent vertex colorings of a graph » (2014)
[2] http://pallini.di.uniroma1.it