Leistungsstarke SAT-Solver-Technologie kann mit der berüchtigten Collatz-Hypothese arbeiten. Die Chancen dafür sind jedoch nicht sehr hoch.
In den letzten Jahren hat Mariin Hijul eine computergestützte Proof-Finding-Technologie namens SAT-Solver (SAT für Erfüllbarkeit) verwendet, um eine beeindruckende Liste mathematischer Probleme zu bewältigen. Pythagoreische Drillinge im Jahr 2016, Schurs Nummer 5 im Jahr 2017 und kürzlich Kellers Hypothese in der siebten Dimension, über die wir vor nicht allzu langer Zeit im Artikel "Die Computersuche hat geholfen, ein 90 Jahre altes mathematisches Problem zu lösen " geschrieben haben.
Jetzt hat Hijul, ein Informatiker an der Carnegie Mellon University, ein noch ehrgeizigeres Ziel im Visier: die Collatz-Vermutung, die von vielen als das schwierigste offene Problem in der Mathematik angesehen wird (und möglicherweise am einfachsten zu formulieren ist). Andere Mathematiker, die von mir erfuhren, dass Khiyul einen solchen Versuch unternahm, waren skeptisch.
"Ich sehe nicht ein, wie dieses Problem mit dem SAT-Löser vollständig gelöst werden kann", sagte Thomas Hales von der University of Pittsburgh, einem führenden Experten für Computerbeweise. Diese Technologie hilft Mathematikern im Wesentlichen, Probleme zu lösen, von denen einige unendlich viele Möglichkeiten haben, indem sie sie in diskrete, endliche Probleme verwandeln.
Wie die anderen war auch Hales vorsichtig, Khiyul zu unterschätzen. „Er ist sehr gut darin, kluge Wege zu finden, um Probleme in der SAT-Sprache zu formulieren. Er ist sehr gut darin. "
Scott AaronsonDie Universität von Texas in Austin arbeitete mit Hiyul an der Collatz-Vermutung und fügte hinzu: „Marin ist ein Mann mit einem Hammer, dh einem SAT-Löser, und wahrscheinlich der würdigste Träger dieses Hammers auf der Welt. Und er versucht es auf fast alles anzuwenden. " Aber nur die Zeit wird zeigen, ob er die Collatz-Hypothese in einen Nagel verwandeln kann.
Die SAT-Lösung erfordert die Neuformulierung der Probleme in einer computerverständlichen Sprache, die Aussagenlogik verwendet , und die anschließende Verbindung von Computern, um zu entscheiden, ob es eine Möglichkeit gibt, diese Aussagen wahr zu machen. Hier ist ein einfaches Beispiel.
Angenommen, Sie sind Eltern und versuchen, eine Kinderbetreuung zu arrangieren. Eine Ihrer Kindermädchen kann die ganze Woche außer Dienstag und Donnerstag arbeiten. Der andere ist außer Dienstag und Freitag. Der dritte - außer Donnerstag und Freitag. Sie müssen am Dienstag, Donnerstag und Freitag mit Ihrem Kind zusammensitzen. Kann das erreicht werden?
Eine Möglichkeit, dies zu testen, besteht darin, die Nanny-Einschränkungen in eine Formel umzuwandeln und sie dem SAT-Solver zuzuführen. Das Programm wird nach einer Möglichkeit suchen, die Tage unter den Kindermädchen zu verteilen, sodass sich herausstellt, dass die Formel wahr oder "zufrieden" ist - das heißt, dass Sie die drei Tage erhalten, die Sie benötigen. Bei Erfolg wird eine solche Methode existieren.
Leider ist nicht sofort klar, wie viele der wichtigsten mathematischen Fragen in die SAT-Sprache umformuliert werden können. Aber manchmal können sie auf unerwartete Weise als Zufriedenheitsfragen umformuliert werden.
"Es ist schwer vorherzusagen, wann die Aufgabe auf eine riesige, aber endliche Berechnung reduziert wird", sagte Aaronson.
Die Collatz-Vermutung ist eine dieser mathematischen Fragen, die auf den ersten Blick überhaupt nicht als Kindermädchenproblem erscheinen. Sie schlägt Folgendes vor: Nehmen Sie eine beliebige Zahl (Ganzzahl, ungleich Null). Wenn es ungerade ist, multiplizieren Sie es mit 3 und addieren Sie 1. Wenn es gerade ist, dividieren Sie durch 2. Als Ergebnis erhalten Sie eine neue Zahl. Wenden Sie die gleichen Regeln an und fahren Sie fort. Die Hypothese sagt voraus, dass Sie unabhängig von der Startnummer 1 erhalten und dann in einer Schleife stecken bleiben: 1, 4, 2, 1.
Und trotz der Tatsache, dass mit dieser Hypothese seit fast 100 Jahren gearbeitet wird, haben Mathematiker es nicht annähernd bewiesen.
Aber das hielt Khiyul nicht auf. 2018 erhielten sie und Aronson als Universitätskollegen von der National Science Foundation ein Stipendium, um den SAT-Löser auf die Collatz-Vermutung anzuwenden.
Nimm eine beliebige Nummer. Wenn es ungerade ist, multiplizieren Sie es mit 3 und addieren Sie 1. Wenn es gerade ist, dividieren Sie durch 2. Als Ergebnis erhalten Sie eine neue Zahl. Wenden Sie die gleichen Regeln an und fahren Sie fort. Können Sie eine Zahl finden, die nicht zu 1 führt? Sie können es selbst versuchen .
Zunächst entwickelte der Informatiker Aaronson eine alternative Formulierung der sogenannten Collatz-Hypothese. Ein "Substitutionsregelsystem", mit dem Computer leichter arbeiten können.
In einem Substitutionsregelsystem arbeiten Sie mit einer Reihe von Zeichen, z. B. den Buchstaben A, B und C. Sie verwenden sie, um Sequenzen zu bilden: ACACBACB. Sie haben auch Regeln zum Konvertieren dieser Sequenzen. Eine Regel könnte besagen, dass Sie einen AC durch BC ersetzen, wenn Sie ihn treffen. Andere können das Flugzeug durch AAA ersetzen. Sie können eine beliebige Anzahl von Regeln definieren, die Transformationen definieren.
Informatiker müssen im Allgemeinen wissen, ob ein bestimmtes Joint Venture immer endet. Das heißt, unabhängig davon, mit welcher Zeile zu beginnen ist und in welcher Reihenfolge die Regeln angewendet werden, ist es wahr, dass die Zeile schließlich in einen Zustand übergeht, in dem keine Regeln angewendet werden können?
Aaronson entwickelte einen SP mit sieben Symbolen und elf Regeln, ähnlich der Hypothese von Collatz. Wenn sie beweisen können, dass sein Joint Venture immer endet, werden sie damit beweisen, dass die Hypothese korrekt ist.
Um Collatz 'Vermutung in ein SAT-Löser-Problem zu verwandeln, mussten Aaronson und Hiyul einen weiteren Schritt mit Matrizen oder Zahlenfeldern unternehmen. Sie mussten jedem Symbol in ihrem SP eine eindeutige Matrix zuweisen. Dieser Ansatz - eine übliche Methode, um nach Beweisen dafür zu suchen, dass der SP die Arbeit beendet - würde es ihnen ermöglichen, über Zahlentransformationen durch Matrixmultiplikation nachzudenken. Sieben Matrizen, die sieben Symbole mit SP bezeichnen, mussten eine ganze Reihe von Einschränkungen erfüllen, die die Entsprechung von 11 Regeln untereinander widerspiegeln.
"Zuerst versuchen Sie, Matrizen zu finden, die diese Einschränkungen erfüllen", sagteEmre Yolchu , Doktorand an der Carnegie Mellon University, arbeitet mit Hijul an diesem Problem. „Wenn Sie Erfolg haben, beweisen Sie, dass die Ausführung stoppt“, und daher ist die Hypothese von Collatz richtig.
Der SAT-Löser kann die Frage nach der Existenz von Matrizen beantworten, die diese Einschränkungen erfüllen. Aaronson und Hijul haben den SAT-Solver zuerst auf kleinen 2x2-Matrizen ausgeführt. Sie fanden keine Arbeitsmöglichkeiten. Dann versuchten sie 3x3-Matrizen. Und wieder ohne Erfolg. Sie vergrößerten die Matrizen weiter in der Hoffnung, dass sie gefunden werden konnten.
Dieser Ansatz kann sich jedoch nicht auf unbestimmte Zeit entwickeln, da die Komplexität der Suche nach geeigneten Matrizen mit ihrer Größe exponentiell zunimmt. Hijul schlägt vor, dass moderne Computer einfach keine Matrizen verarbeiten können, die größer als 12 x 12 sind.
"Wenn die Matrizen zu komplex werden, können Sie das Problem nicht lösen", sagte er.
Hijul arbeitet immer noch an der Optimierung der Suche und versucht, sie effizienter zu gestalten, damit der SAT-Solver immer größere Matrizen überprüfen kann. Sie und ihre Kollegen arbeiten an einem Artikel, der ihre aktuellen Entdeckungen zusammenfasst, aber sie haben fast keine Ideen mehr und müssen wahrscheinlich bald aufgeben - zumindest für eine Weile.
Schließlich besteht die Attraktion des SAT-Lösers darin, dass Sie wahrscheinlich finden könnten, wonach Sie suchen, wenn Sie nur herausfinden könnten, wie Sie einen anderen Fall überprüfen, ein anderes Kindermädchen anrufen und die Suche auch nur für eine kurze Zeit verlängern können. In diesem Sinne ist Khiyuls Hauptvorteil möglicherweise nicht seine Erfahrung mit SAT-Lösern, sondern seine Liebe zum Streben nach Ergebnissen.
"Ich bin nur ein Optimist", sagte er. "Ich habe oft das Gefühl, Glück zu haben, also versuche ich nur zu sehen, wie weit ich kommen kann."