Heule empfand die Entdeckung früherer Ergebnisse jedoch als belebend. Es zeigte, dass andere Forscher das Problem für wichtig genug hielten, um daran zu arbeiten, und bestätigte für ihn, dass das einzige erzielbare Ergebnis darin bestand, das Problem vollständig zu lösen.
„Als wir herausfanden, dass an dem Problem 20 Jahre lang gearbeitet worden war, veränderte sich das Bild völlig“, sagte er.
Das Vulgäre meiden
Im Laufe der Jahre hatte Heule es sich zur Aufgabe gemacht, effiziente Methoden zur Suche in einer Vielzahl möglicher Kombinationen zu finden. Sein Ansatz heißt SAT-Lösung – kurz für „Satisfiability“. Dabei wird eine lange Formel, eine sogenannte boolesche Formel, erstellt, die zwei mögliche Ergebnisse haben kann: 0 oder 1. Wenn das Ergebnis 1 ist, ist die Formel wahr und das Problem ist erfüllt.
Für das Problem der Packungsfärbung könnte jede Variable in der Formel darstellen, ob eine bestimmte Zelle mit einer bestimmten Zahl besetzt ist. Ein Computer sucht nach Möglichkeiten, Variablen zuzuordnen, um die Formel zu erfüllen. Wenn der Computer dazu in der Lage ist, wissen Sie, dass es möglich ist, das Raster unter den von Ihnen festgelegten Bedingungen zu packen.
Leider könnte sich eine einfache Codierung des Packungsfärbungsproblems als boolesche Formel auf viele Millionen Begriffe erstrecken – ein Computer oder sogar eine Flotte von Computern könnte endlos laufen und alle verschiedenen Möglichkeiten der darin enthaltenen Variablenzuweisungen testen.
„Der Versuch, diese rohe Gewalt anzuwenden, würde, wenn man es naiv täte, bis zum Ende des Universums dauern“, sagte Goddard. „Man braucht also ein paar coole Vereinfachungen, um es auf etwas zu reduzieren, das überhaupt möglich ist.“
Darüber hinaus wird es jedes Mal, wenn Sie dem Problem der Packungsfärbung eine Zahl hinzufügen, aufgrund der Art und Weise, wie sich die möglichen Kombinationen vervielfachen, etwa 100-mal schwieriger. Das heißt, wenn eine Bank parallel arbeitender Computer 12 an einem einzigen Rechentag ausschließen könnte, bräuchte sie 100 Tage Rechenzeit, um 13 auszuschließen.
Heule und Subercaseaux betrachteten die Skalierung eines Brute-Force-Rechenansatzes in gewisser Weise als vulgär. „Wir hatten mehrere vielversprechende Ideen, also haben wir uns vorgenommen: ‚Lasst uns versuchen, unseren Ansatz zu optimieren, bis wir dieses Problem in weniger als 48 Stunden Rechenzeit auf dem Cluster lösen können‘“, sagte Subercaseaux.
Dazu mussten sie Möglichkeiten finden, die Anzahl der Kombinationen zu begrenzen, die der Computercluster ausprobieren musste.
„[They] Ich möchte es nicht nur lösen, sondern auf beeindruckende Weise“, sagte er Alexander Soifer der University of Colorado, Colorado Springs.
Heule und Subercaseaux erkannten, dass viele Kombinationen im Wesentlichen gleich sind. Wenn Sie versuchen, ein rautenförmiges Plättchen mit acht verschiedenen Zahlen zu füllen, spielt es keine Rolle, ob die erste Zahl, die Sie platzieren, eine oben und eine rechts vom Mittelquadrat oder eine unten und eine links davon ist das mittlere Quadrat. Die beiden Platzierungen sind symmetrisch zueinander und schränken Ihren nächsten Zug auf genau die gleiche Weise ein, es gibt also keinen Grund, sie beide zu überprüfen.
Wenn jedes Packproblem mit einem Schachbrettmuster gelöst werden könnte, bei dem ein diagonales Einsengitter den gesamten Raum abdeckt (wie die dunklen Felder auf einem Schachbrett), könnten die Berechnungen erheblich vereinfacht werden. Dies ist jedoch nicht immer der Fall, wie in diesem Beispiel einer endlichen Kachel mit 14 Zahlen. Das Schachbrettmuster muss an einigen Stellen nach links oben unterbrochen werden.Mit freundlicher Genehmigung von Bernardo Subercaseaux und Marijn Heule