Coloration de graphe

Cet article est une ébauche à compléter, vous pouvez partager vos connaissances en le modifiant.
Sommaire

Définition

Il existe deux façons de colorer un graphe.

Propriétés

Méthodes

Algorithme de Welsh et Powell

  1. Repérer le degré de chaque sommet.
  2. Ranger les sommets par ordre de degrés décroissants. (dans certains cas plusieurs possibilités)
  3. Attribuer au premier sommet (A) de la liste une couleur.
  4. Suivre la liste en attribuant la même couleur au premier sommet (B) qui ne soit pas adjacent à (A).
  5. Suivre (si possible) la liste jusqu'au prochain sommet (C) qui ne soit adjacent ni à A ni à B.
  6. Continuer jusqu'à ce que la liste soit finie.
  7. Prendre une deuxième couleur pour le premier sommet (D) non encore colorié de la liste.
  8. Répéter les operations 4 à 6.
  9. Continuer jusqu'à avoir colorié tous les sommets.

Cette méthode n'aboutit pas forcément à une coloration minimale. Il faut donc observer si on peut faire mieux (c'est-à-dire avec moins de couleurs).

Partition en sous-graphes stables

Un sous-graphe stable est un sous-graphe dont les sommets ne sont pas adjacents. Ses sommets peuvent donc être colorés de la même couleur. Le but est de trouver un nombre minimal de sous-graphes stables pour utiliser le moins de couleurs possible.

Applications

Le théorème des quatre couleurs

Peut-on colorier une carte avec quatre couleurs de sorte que deux pays ayant une frontière commune (autre que réduite à un point) n'aient jamais la même couleur?

On ne trouvait pas de contre-exemple de cette affirmation empirique. Restait à la démontrer.

Une démonstration publiée en 1879 par Kempe, s'est révélée comporter une erreur. Il a fallu attendre près d'un siècle de recherche pour voir aboutir une démonstration valide.

En 1976, deux américains Kenneth Appel et Wolfgang Haken affirment avoir démontré le théorème des quatre couleurs. Leur démonstration partage la communauté scientifique : pour la première fois, en effet, la démonstration exige l'usage de l'ordinateur pour étudier les 1200 cas critiques. Le problème de la validation du théorème se trouve alors déplacé vers le problème de la validation :

Depuis 1976, l'algorithme d'Appel et Haken a été repris et simplifié par d'autres chercheurs. D'autres programmes informatiques, écrits de façon indépendante du premier, aboutissent au même résultat. Il existe ainsi une version entièrement formalisée de la preuve, formulée avec Coq.

Organisation

Permet d'optimiser :

See also: Coloration de graphe, 1976, Coq (logiciel), Degré, Homomorphisme, NP-Complet, Théorie des graphes, Vérification formelle