Théorème des quatre couleurs
Un article de Wikipédia, l'encyclopédie libre.
.png/300px-Federal_subjects_of_Russia_(by_number).png)
Notons d'emblée un point de vocabulaire : en théorie des graphes on parle de coloration de graphe, on dira donc colorer et non colorier, colorer signifiant plus mettre en reflet tandis que colorier implique l'action de choisir concrètement une couleur comme jaune ou rouge. Ceci se justifie par le fait que colorer un graphe consiste essentiellement à en révéler sa structure (en l'occurrence, est-il k-parti ou non ?). Le coloriage concret du graphe ne présente aucun intérêt puisque du point de vue mathématique les couleurs sont abstraites et interchangeables.
Le Théorème des quatre couleurs affirme qu'il est possible, en n'utilisant que quatre couleurs différentes, de colorer n'importe quelle carte découpée en régions connexes, de sorte que deux régions adjacentes (idem limitrophes) reçoivent toujours deux couleurs distinctes. L'énoncé peut varier et concerner, de manière tout à fait équivalente, la coloration des faces d'un polyèdre, ou des sommets d'un graphe planaire.
Trivialement, chacune des régions doit recevoir une couleur différente si les régions sont deux-à-deux adjacentes, c'est le cas par-exemple de la Belgique, du Luxembourg, de l'Allemagne et de la France dans une carte politique de l'Europe. D'où la nécessité des quatre couleurs dans le cas général. Par ailleurs, il ne peut exister cinq régions connexes deux-à-deux adjacentes (c'est la partie facile du théorème de Kuratowski).
Lorsqu'on généralise le problème à un graphe quelconque, il devient NP-complet de déterminer s'il est colorable avec seulement 4 couleurs (et même 3).
Sommaire |
[modifier] Histoire
Le résultat fut conjecturé en 1852 par Francis Guthrie, intéressé par la coloration de la carte des régions d'Angleterre. La première mention publiée date toutefois de 1879[1]. Deux premières démonstrations furent publiées, respectivement par Kempe en 1879 et par Peter Guthrie Tait en 1880. Mais elles s'avèrent erronées ; les erreurs ont été relevées seulement en 1890 par Percy Heawood et en 1891 par Julius Petersen.
Ironiquement la fausse preuve de Kempe contient le schéma général de la vraie preuve. La fausse preuve fournit en fait une démonstration du résultat analogue mais avec cinq couleurs au lieu de quatre, aujourd'hui connu sous le nom du théorème des cinq couleurs (dont l'unique intérêt est d'admettre une courte preuve, donnée dans la référence), comme l'a remarqué Percy Heawood en 1890.
Dans les années 1960 et 1970, Heinrich Heesch s'intéresse à la possibilité de prouver informatiquement le théorème des quatre couleurs. Finalement, 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 1478 cas critiques (plus de 1200 heures de calcul). Le problème de la validation du théorème se trouve alors déplacé vers le problème de la validation :
- d'une part de l'algorithme d'exploration ;
- d'autre part de sa réalisation sous forme de programme.
Depuis 1976, l'algorithme d'Appel et Haken a été repris et simplifié par Robertson, Sanders, Seymour et Thomas. 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, formulée avec Coq par Georges Gonthier et Benjamin Werner, qui prouve le théorème des quatre couleurs.
Paul Erdös pensait que le théorème des quatre couleurs était « un problème subtil et non pas un problème complexe ». D'après lui, une démonstration simple, et même très simple, devait exister. Mais pour cela, il aurait fallu « compliquer le problème » et imaginer la formulation d'un ensemble de points plus vaste qu'un graphe-plan et incluant celui-ci. En 1980, George Spencer-Brown déposa une preuve du théorème des quatre couleurs à la Royal Society[2], mais qui n'a été ni acceptée ni invalidée aujourd'hui.
[modifier] Généralisation du théorème des quatre couleurs
L'énoncé classique du théorème des quatre couleurs n'est bien sûr pas une caractérisation des graphes dont le nombre chromatique est inférieur ou égale à 4 puisque le K3,3 n'est pas planaire mais est biparti. D'autre part, pour des raisons de complexité algorithmique, il ne peut exister de caractérisation simple des graphes k-colorables pour k fixé supérieur à 3. Le théorème des quatre couleurs se généralise aux graphes sans mineur K5, puisque le nombre chromatique de ces graphes vaut au plus 4 (et c'est une des motivations de la conjecture d'Hadwiger). Une généralisation plus forte encore a été donnée récemment par Guenin :
- les graphes sans mineur impair K5 sont colorables avec seulement 4 couleurs.
- (Un mineur est dit impair si les opérations de suppressions et de contractions des arêtes s'effectuent uniquement sur une coupe du graphe. Un graphe contient un mineur impair K5 s'il contient un K5 dont on a remplacé les dix arêtes par dix chemins de longueur impairs.)
Ces résultats plus forts sont basés sur des preuves utilisant le théorème des quatre couleurs lui-même, par-conséquent ils ne fournissent pas de nouvelles preuves du fameux théorème.
[modifier] Utilisation pratique
D’autres problèmes plus pratiques peuvent se réduire à la résolution de coloration de graphe, la solution peut alors être appliquée pour améliorer l'organisation de tâches.
- Affecter des fréquences différentes à des cellules voisines dans un réseau de téléphone mobile GSM.
- Organiser un examen suivant les matières que doit passer chaque étudiant. Comment mettre en parallèle plusieurs épreuves sans léser un candidat ?
- Optimiser l'utilisation des machines de travail. Comment mettre en parallèle des fabrications utilisant plusieurs machines ?
- Problème d'incompatibilité. Comment faire cohabiter des personnes ou animaux en tenant compte de leur incompatibilité ?
