Zahlen, bitte! Mit 800 CPU-Kernen zur Zahl 7825

Drei Forscher haben sich aufgemacht, das Problem boolescher pythagoräischer Zahlentripel zu lösen und ein symbolisches Preisgeld von immerhin 100 US-Dollar abgesahnt. Äh, was sind eigentlich pythagoräische Zahlentripel?

In Pocket speichern vorlesen Druckansicht 117 Kommentare lesen
Zahlen, bitte! 7825
Lesezeit: 4 Min.
Von
  • Volker Zota
Zahlen, bitte!

In dieser Rubrik stellen wir immer dienstags verblüffende, beeindruckende, informative und witzige Zahlen aus den Bereichen IT, Wissenschaft, Kunst, Wirtschaft, Politik und natürlich der Mathematik vor.

Den Satz des Pythagoras und die Gleichung a2 + b2 = c2 dürften so ziemlich alle aus ihrem Matheunterricht kennen. Manche erinnern sich vielleicht auch an die Zwölfknotenschnur, mit der man einen rechten Winkel darstellen kann, indem man ein Dreieck mit Kantenlängen 3:4:5 legt. Das klappt, weil die Zahlen eben den Satz des Pythagoras 32 + 42 = 9 + 16 = 25 = 52 erfüllen. Solche ganzzahlige Lösungen der Gleichung nennt man "pythagoräische Zahlentripel". Andere kleine pythagoräische Zahlentripel sind beispielsweise 52 + 122 = 132 oder 62 + 82 = 102. Und wo ist jetzt das Problem?

Mathematiker haben bekanntermaßen einen angeborenen Spaß an Zahlenrätseln und Fragen, die sich sonst keiner stellt. Auftritt des bekannten US-Mathemagikers Ronald Graham: Er lobte in den achtziger Jahren ein symbolisches Preisgeld in Höhe von 100 US-Dollar für diejenigen aus, die das aus der Ramsey-Theorie stammende kombinatorische Problem boolescher pythagoräischer Zahlentripel lösen. Die Fragestellung lautet: Kann man die Zahlen von 1 bis n so in zwei Gruppen (rot oder blau eingefärbt) aufteilen, dass keine von beiden ein pythagoräisches Tripel enthält? Sprich, es dürfen nicht alle drei Zahlen eines solchen Tripels dieselbe Farbe haben.

Für kleine n kann man das noch durchprobieren. Allerdings wird es schnell unübersichtlich, weil es 2n Möglichkeiten gibt; schon bei n = 100 wären es schon mehr als 1030 Möglichkeiten. Also haben die drei Forscher Marijn J. H. Heule, Oliver Kullmann und Victor W. Marek die 800 CPU-Kerne des Stampede Supercomputers (Texas Advanced Computing Center) auf das Problem angesetzt. Dabei kam heraus, dass die Färbung bis n = 7824 klappt, danach aber nicht mehr.

Hätten sie nur blind alle Möglichkeiten durchprobieren lassen, müsste man noch lange auf das Ergebnis warten, denn auch ein Supercomputer würde sich an dem Problem die Zähne ausbeißen, wenn man sich nicht geschickt anstellt; immerhin wären 27825 = 3,63 × 102355 Möglichkeiten zu prüfen.

Lösung für n = 7824; für höhere n klappt es nicht mehr (bei den weißen Zahlen ist die Färbung beliebig, kann also blau oder rot sein.)

(Bild: Marijn Heule)

Darum haben sie ihre selbst entwickelte "Cube & Conquer"-Methode angewandt, die sich besonders gut für große kombinatorische Probleme eignet. Dazu haben die Forscher zunächst die Fragestellung in ein Erfüllbarkeitsproblem (SAT, englisch "Satisfiability") kodiert, dieses zwecks effizienter Verarbeitung transformiert, aufgeteilt und schließlich dessen Unerfüllbarkeit ab n = 7285 bewiesen.

Schema der computergestützten Beweisführung

(Bild: Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek )

So konnte die Rechenzeit des Supercomputers auf nur zwei Tage gedrückt werden. Der Beweis hat im DRAT-Format (Deletion Resolution Asymmetric Tautology) eine Gesamtgröße von 200 Terabyte und wird darum als bisher "größter" mathematischer Beweis aller Zeiten gefeiert.

Die Wissenschaftler haben alle einzelnen Beweisschritte durch Software – Theorembeweiser und Beweis-Checker – auf Richtigkeit geprüft. Der Datensatz (komprimiert 68 GByte) steht zur Kontrolle durch Dritte zur Verfügung. Interessierte finden die vom Autoren hier verschwiegenen (und sein Verständnis übersteigenden) Details in der Veröffentlichung "Solving and Verifying the boolean PythagoreanTriples problem via Cube-and-Conquer" (PDF).

So richtig befriedigend ist der maschinengestützte Beweis aber nicht. Den meisten Mathematikern ist eine klassische Beweisführung lieber, bei der dann hoffentlich auch klar werden würde, warum das Einfärben ausgerechnet ab n = 7825 nicht mehr funktioniert. Möglicherweise liefert das Resultat aber Denkanstöße für einen Beweis ohne Computer-Unterstützung.

Für Ron Graham haben Heule, Kullmann und Marek die Herausforderung aber erfüllt. Er hat ihnen kürzlich die 100 US-Dollar als symbolischen Preis überreicht, was laut den Wissenschaftlern nicht einmal die Stromrechnung für den Beweis decken würde ... (vza)