Der Vier-Farb-Satz

The Four Color Theorem
Copyright © Robin Thomas
For original English text, go to: http://people.math.gatech.edu/~thomas/FC/fourcolor.html
Translated by Valeria Aleksandrova

Diese Seite bietet die Kurzzusammenfassung eines neues Beweises des Vier-Farben-Satzes und einen Vierfarbalgorithmus, der von Neil Robertson, Daniel P. Sanders, Paul Seymour und Robin Thomas gefunden wurde.



Inhalt:

  1. Geschichte
  2. Warum ein neuer Beweis?
  3. Beweisskizze
  4. Hauptmerkmale unseres Beweises
  5. Konfigurationen
  6. Regeln zum Entladen
  7. Verweise
  8. Ein quadratischer Algorithmus.
  9. Diskussion
  10. Quellen


Geschichte:

Der Vier-Farben-Satz wird auf das Jahr 1852 datiert, als Francis Guthrie, der gerade eine Karte der englischen Grafschaften ausmalte, bemerkte, dass vier Farben dafür ausreichten. Er fragte seinen Bruder Frederick, ob es wahr sei, dass jede Karte mit nur vier Farben so ausgemalt werden kann, dass angrenzende Regionen (d.h. solche, die einen kompletten Grenzabschnitt teilen, nicht nur einen Punkt) verschiedene Farben erhalten. Frederick gab die Vermutung an DeMorgan weiter. Die erste schriftlich fixierte Quelle stammt von Cayley, 1878.

Ein Jahr später erschien der erste ‘Beweis’ von Kempe; seine Unrichtigkeit wurde elf Jahre später von Heawood herausgestellt. Ein anderer Beweis, der versagt hat, beruht auf Tait im Jahr 1880; eine Lücke in der Argumentationskette wurde 1891 von Petersen herausgestellt. Indes besaßen die beiden falschen Beweise einen gewissen Wert. Kempe entdeckte das, was später als Kempe-Ketten bekannt wurde, und Tait fand eine äquivalente Formulierung des Vier-Farb-Satzes hinsichtlich der Drei-Ecken-Färbung. .

Der Hauptbeitrag stammt von Birkhoff, dessen Arbeit es Franklin 1922 erlaubte, den Beweis für die Richtigkeit der Vier-Farb-Vermutung für Karten mit bis zu 25 Regionen zu erbringen. Sie wurde auch von anderen Mathematikern genutzt, um vielfältige Fortschritte beim Vier-Farb-Problem zu erzielen. Besondere zu nennen ist Heesch, der die zwei Bestandteile entwickelte, die für den endgültigen Beweis notwendig sind – Reduzierbarkeit und Entladen. Während das Konzept der Reduzierbarkeit auch von anderen Forschern studiert wurde, scheint es, als ob die Idee des Entladens, die zwingend notwendig ist für den Unvermeidbarkeitsabschnitt des Beweises, auf Heesch beruht, und dass er es war, der mutmaßte, dass eine angemessene Entwicklung dieser Methode das Vier-Farb-Problem lösen würde.

Bewiesen wurde dies von Appel und Haken im Jahr 1976, als sie ihren Beweis des Vier-Farb-Satzes  [1,2] veröffentlichten.

Warum eine neuer Beweis?

Es gibt zwei Gründe, warum der Appel-Haken-Beweis nicht vollständig zufriedenstellend ist:

  • Zum Teil wird für den Appel-Haken-Beweis ein Computer genutzt, weswegen dieser nicht manuell verifiziert werden kann, und
  • Selbst der Teil, der angenommenerweise von Hand überprüft werden kann, ist außerordentlich kompliziert und langweilig, und soweit wir wissen, hat niemand ihn jemals in voller Gänze überprüft

Tatsächlich haben wir versucht, den Appel-Haken-Beweis zu überprüfen, das aber schnell wieder aufgegeben. Den Computerteil zu überprüfen, würde nicht nur eine Menge Programmierarbeit bedeuten, sondern auch die Eingabe der Beschreibungen 1476 Graphen, und das war noch nicht einmal der brisanteste Teil des Beweises.

Wir hielten es für profitabler, unseren eigenen Beweis auszuarbeiten. Das haben wir getan und haben nun einen Beweis und einen Algorithmus, die beide unten beschrieben stehen.

Beweisskizze

Die Grundidee des Beweises ist dieselbe wie bei Appel und Haken. Wir stellen ein Set von 633 „Konfigurationen“ dar und beweisen, dass jede von ihnen „reduzierbar“ ist. Dies ist ein technisches Konzept, welches voraussetzt, dass keine Konfiguration mit diesem Merkmal als minimales Gegenbeispiel zum Vier-Farb-Satz auftreten kann. Es kann auch in einem Algorithmus benutzt werden, denn wenn eine reduzierbare Konfiguration in einem planaren Graphen G auftritt, dann kann man in andauernder Zeit einen kleineren planaren Graphen G’ konstruieren, sodass jede Vier-Färbung von G’ in linearer Zeit zu einer Vier-Färbung von G konvertiert werden kann.

Seit 1913 ist bekannt, dass jedes minimale Gegenbeispiel zum Vier-Farb-Satz intern eine sechsfach verbundene Triangulation ist. Im zweiten Teil des Beweises beweisen wir, dass wenigstens eine unserer 633 Konfigurationen in jeder internen sechsfach verbundenen ebenen Triangulation erscheint (nicht notwendig ein minimales Gegenbeispiel zum 4CT). Dies wird Unvermeidbarkeitsbeweis genannt, und dafür wird die Entlastungs-Methode, die Heesch als Erster vorschlug, genutzt. Hier unterscheidet sich unsere Methode von der Appels und Hakens.

Hauptmerkmale unseres Beweises:

Wir bekräftigen eine Vermutung Heeschs, dass beim Beweis der Unvermeidbarkeit eine reduzierbare Konfiguration in der zweiten Nachbarschaft eines „überladenen“ Eckpunktes gefunden werden kann; so vermeiden wir „Immersions“-Probleme, die für Appel und Haken eine Hauptkomplikationsquelle darstellten. Unser unvermeidbares Set besteht aus 633 Teilen, gegenüber dem 1476-Stück-Set von Appel und Haken, und unsere Entlastungsmethode benutzt nur 32 Entlastungsregeln, anstelle der über 300 Stück bei Appel und Haken. Zuletzt haben wir einen quadratischen Algorithmus für vierfarbige planare Graphen (Beschreibung später), eine Verbesserung gegenüber Appels und Hakens biquadratischem Algorithmus.

Konfigurationen:

Eine Beinahe-Triangulation ist ein non-null verbundener, schleifenloser, ebener Graph, sodass jede finite Region eine Triangel ist. Eine Konfiguration K besteht aus einer Beinahe-Triangulation G und einer Karte g von V(G) zu den Ganzzahlen mit den folgenden Eigenschaften:

  1. für jeden Knoten v hat G\v höchstens zwei Komponente und wenn es zwei sind, dann ist der Grad von v, g(v)-2,
  2. für jeden Knoten v, wenn v nicht mit der unendlichen Fläche verbunden ist, dann ist g(v) gleich dem Grad von v, und anderenfalls ist g(v) größer als der Grad von v, und in beiden Fällen g(v)>4
  3. K hat Ringgröße mindestens 2, wo die Ringgröße von K als die Summe von g(v)-deg(v)-1, summiert über alle Knoten v verbunden mit der unendlichen Fläche, sodass G\v verbunden ist.

Beim Zeichnen der Konfigurationen nutzen wir eine von Heesch eingeführte Konvention. Die Formen der Knoten geben den Wert von g(v) wie folgt an: Ein solider schwarzer Kreis bedeutet g(v)=5, ein Punkt (oder das, was im Bild gar nicht als Symbol erscheint) heißt g(v)=6, ein hohler Kreis bedeutet g(v)=7, ein hohles Viereck heißt g(v)=8, ein Dreieck ist g(v)=9 und ein Fünfeck heißt g(v)=10. (Wir brauchen keine Punkte v mit g(v)>11, und nur einen Punkt mit g(v)=11, für den wir kein spezielles Symbol verwenden). Im unteren Bild werden 17 unserer 633 reduzierbaren Konfigurationen mit den angegebenen Konventionen dargestellt. Das ganze Set kann hier angeschaut werden. (Wir verweisen für die Bedeutung von „dicken Ecken“ und „Halbecken“ in diesen Bildern auf (3.2) unseres Aufsatzes [7]).

Jede Konfiguration, die zu einer der in [7] dargestellten 633 Konfigurationen isomorph ist, wird als gute Konfiguration bezeichnet. Lass T eine Triangulation sein. Eine Konfiguration K=(G,g) erscheint in T, wenn G ein indizierter Teilgraph von T ist, ist jede endliche Fläche von G eine Fläche von T, und g(v) ist gleich dem Grad (degree) von v in T für jeden Knoten v von G. Wir beweisen die folgenden beiden Aussagen:

THEOREM 1.

Wenn T ein minimales Gegenbeispiel zum Vier-Farb-Satz ist, erscheint in T keine gute Konfiguration.

THEOREM 2.

Bei jeder intern sechsfach verbundenen Triangulation T, erscheinen in T einige gute Konfigurationen.

Aus den beiden obigen Theoremen ergibt sich, dass keine minimalen Gegenbeispiele existieren, und daher ist der Vier-Farb-Satz wahr. Der erste Beweis benötigt die Unterstützung eines Computers. Der zweite kann von Hand in wenigen Monaten bewiesen werden, oder, mit der Hilfe eines Computers, in etwa 20 Minuten.

Regeln zum Entladen:

In der Annahme, dass T eine intern sechsfach verbundene Triangulation ist: Einleitend ist jedem Knoten v die Charge („Ladung“) 10(6-deg(v)) zugewiesen. Aus Eulers Formel folgt, dass die Summe der Chargen aller Knoten 120 beträgt; speziell ist sie positiv. Wir verteilen die Chargen nun nach den folgenden Regeln um: Wann immer T einen Teilgraphen hat, der isomorph ist zu einem der Graphen in der unteren Darstellung und die Gradspezifikationen erfüllt (für einen Knoten v einer Regel mit einem Minuszeichen nahe v, bedeutet dies, dass der Grad der korrespondierenden Ecke von T meistens der Wert ist, der durch die Form von v spezifiziert ist, und analog für Eckpunkte mit einem Pluszeichen nahebei; gleiches gilt auch für Ecken ohne Zeichen), wird eine Charge von eins (zwei im Fall der ersten Regel) die Ecke entlanggesendet, die mit einem Pfeil markiert ist.

Diese Prozedur definiert ein neues Chargen-Set mit demselben Endergebnis. Da die Endsumme positiv ist, gibt es in T einen Knoten v, dessen neue Charge positiv ist. Wir zeigen, dass eine gute Konfiguration in der zweiten Nachbarschaft von v erscheint.

Wenn der Grad (degree) von v höchstens 6 oder mindestens 12 ist, kann dies recht einfach durch einen direkten Beweis gesehen werden. In den verbleibenden Fällen sind die Beweise allerdings schwieriger zu erbringen. Daher haben wir die Beweise in formaler Sprache [bzw. Formensprache] geschrieben, sodass sie von einem Computer verifiziert werden können. Jeder Einzelschritt dieser Beweise ist auch menschlich verifizierbar, doch die Beweise sind aufgrund ihrer Länge nicht wirklich manuell überprüfbar.

Verweise:

Der theoretische Teil unseres Beweises wird in [7] beschrieben. Ein zehnseitige r Überblick ist online verfügbar. Die Computerdaten und Programme waren bisher auf einem anonymen ftp-Server, doch dieser Server wurde abgebaut. Dieselben Dateien sind nun über http://www.math.gatech.edu/~thomas/OLDFTP/four/ erhältlich und können bequem angeschaut werden. Ein unabhängiges Programmset würde von von Gasper Fijavz unter der Leitung von Bojan Mohar geschrieben.

Ein quadratischer Algorithmus:

Der Input zum Algorithmus wird eine ebene Triangulation G mit n Knoten sein (dies ist kein Generalisierungsverlust, da jeder planare Graph in linearer Zeit trianguliert werden kann). Der Output wird die Einfärbung der Knoten von G mit vier Farben sein.

Wenn G höchstens vier Knoten hat, gib jedem Punkt eine andere Farbe. Wenn anderenfalls G einen Knoten x mit dem Grad k < 5 hat, dann ist der umrundende Kreis C ein ‘k-Ring’. Gehe zur k-Ring-Analyse unten.

Anderenfalls hat G den Mindestgrad 5. Für jeden Eckpunkt berechnen seine Charge, wie oben erklärt, und finden einen Knoten mit positiver Charge. Aus unserem Beweis des 2. Theorems folgt, dass entweder eine gute Konfiguration in der zweiten Nachbarschaft von v auftaucht (dann kann sie in linearer Zeit gefunden werden), oder ein k-Ring, der die Definition der internalen Sechsfachverbindung verletzt, kann in linearer Zeit gefunden werden. Im letzteren Fall gehen wir zur k-Ring-Analyse unten, im ersteren wenden wir die Rekursion auf einen bestimmten kleineren Graphen an. Eine Vierfärbung von G kann dann von der Vierfärbung dieses kleineren Graphen in linearer Zeit konstruiert werden.

Wenn ein k-Ring gegeben ist, der die Definition der internalen Sechsfachverbindung verletzt, kann eine von Birkhoff entwickelte Prozedur genutzt werden. Wir wenden Rekursion auf w´zwei sorgfältig ausgewählte Teilgraphen von G an. Die Vierfach-Farbe von G kann dann von der Vierfärbung der beiden kleineren Graphen in linearer Zeit konstruiert werden.

Diskussion:

Erwähnen sollten wir, dass unsere beiden Programme nur ganzzahlige Arithmetik verwenden, weswegen wir uns nicht um Rundungsfehler und gleichartige Probleme der Gleitkommaarithmetik sorgen müssen. Nichtsdestotrotz kann eingewendet werden, dass unser ‘Beweis’ kein Beweis im herkömmlichen Sinne ist, weil er Schritte beinhaltet, die von Menschen niemals nachvollzogen werden können. Im Besonderen haben wir weder die Korrektheit der Compiler, auf denen wir unsere Programme kompilierten, noch die Unfehlbarkeit der Hardware, auf der unsere Programme liefen, bewiesen. Diese müssen guten Glaubens vorausgesetzt werden, und sind eine vorstellbare Fehlerquelle. Von einem praktischen Gesichtspunkt aus ist aber die Chance, dass ein Computerfehler fortwährend und auf dieselbe Art und Weise, bei allen Durchläufen unserer Programme, auf allen Compilern und allen Betriebssystemen auftritt, verschwindend gering – verglichen mit der Chance eines menschlichen Fehlers während derselben Zeit von Fallprüfung. Abgesehen von dieser hypothetischen Möglichkeit, dass ein Computer fortlaufend eine unwahre Antwort gibt, kann der Rest unseres Beweises auf dieselbe Art verifiziert werden wie traditionelle mathematische Beweise. Wir räumen jedoch ein, dass die Verifizierung eines Computerprogramms sehr viel komplizierter ist, als einen mathematischen Beweis derselben Länge zu überprüfen.

Danksagung:

Unsere Schuld gilt Thomas Fowler, Christopher Carl Heckman und Barrett Walls für ihre Hilfe mit dem Aufbau dieser Seite. Unsere Arbeit wurde teilweise von der National Science Foundation unterstützt.

Quellen:

  1. K. Appel and W. Haken, Every planar map is four colorable. Part I. Discharging, Illinois J. Math. 21 (1977), 429-490.
  2. K. Appel, W. Haken and J. Koch, Every planar map is four colorable. Part II. Reducibility, Illinois J. Math. 21 (1977), 491–567.
  3. K. Appel and W. Haken, Every planar map is four colorable, Contemporary Math. 98 (1989).
  4. G. D. Birkhoff, The reducibility of maps, Amer. J. Math. 35 (1913), 114-128.
  5. H. Heesch, Untersuchungen zum Vierfarbenproblem, Hochschulskriptum 810/a/b, Bibliographisches Institut, Mannheim 1969.
  6. A. B. Kempe, On the geographical problem of the four colors, Amer. J. Math., 2 (1879), 193-200.
  7. N. Robertson, D. P. Sanders, P. D. Seymour and R. Thomas, The four colour theorem, J. Combin. Theory Ser. B. 70 (1997), 2-44.
  8. N. Robertson, D. P. Sanders, P. D. Seymour and R. Thomas, A new proof of the four colour theorem, Electron. Res. Announc. Amer. Math. Soc. 2 (1996), 17-25 (electronic).
  9. T.L. Saaty, Thirteen colorful variations on Guthrie’s four-color conjecture, Amer. Math. Monthly 79 (1972), 2-43.
  10. T.L. Saaty and P. C. Kainen, The four-color problem. Assaults and conquest, Dover Publications, New York 1986.
  11. P. G. Tait, Note on a theorem in geometry of position, Trans. Roy. Soc. Edinburgh 29 (1880), 657-660.
  12. H. Whitney and W. T. Tutte, Kempe chains and the four colour problem”, in Studies in Graph Theory, Part II (ed. D. R. Fulkerson), Math. Assoc. of America, 1975, 378-413.

13. November 1995. Link-Update 8. November 2007.