Forskere løser et 90 år gammelt geometriproblem

Carnegie Mellon University dataloger og matematikere har løst den sidste, stædig del af Kellers formodning, et geometriproblem, som videnskabsmænd har undret sig over i 90 år.

Ved at strukturere puslespillet som det, dataloger kalder et tilfredshedsproblem, forskerne bragte problemet til livs med fire måneders vanvittig computerprogrammering og kun 30 minutters beregning ved hjælp af en klynge af computere.

"Jeg var rigtig glad, da vi løste det, men så var jeg lidt ked af, at problemet var væk, " sagde John Mackey, en lærerprofessor i Datalogi-afdelingen (CSD) og Institut for Matematiske Videnskaber, som havde forfulgt Kellers formodning, siden han var kandidatstuderende for 30 år siden. "Men så følte jeg mig glad igen. Der er bare denne følelse af tilfredshed."

Løsningen var endnu en succes for en tilgang udviklet af Marijn Heule, en lektor i datalogi, der sluttede sig til CSD i august sidste år. Heule har brugt en SAT-løser - et computerprogram, der bruger propositionel logik til at løse tilfredsstillelsesproblemer (SAT) - til at overvinde adskillige grå matematiske udfordringer, inklusive det pythagoriske tripleproblem og Schur nummer 5.

"Problemet har fascineret mange mennesker i årtier, næsten et århundrede, " sagde Heule om Kellers formodning. "Dette er virkelig et udstillingsvindue for, hvad der kan gøres nu, som ikke var muligt tidligere."

Formodningen, stillet af den tyske matematiker Eduard Ott-Heinrich Keller, har at gøre med flisebelægning - specifikt, hvordan man dækker et område med lige store fliser uden huller eller overlap. Formodningen er, at mindst to af fliserne skal dele en kant, og at dette gælder for rum af enhver dimension.

Det er nemt at bevise, at det er sandt for todimensionelle fliser og tredimensionelle terninger. Fra 1940 formodningen var blevet bevist sand for alle dimensioner op til seks. I 1990, imidlertid, matematikere beviste, at det ikke virker ved dimension 10 eller derover.

Det var da Kellers formodning fangede Mackeys fantasi, derefter studerende ved University of Hawaii. Med et kontor ved siden af ​​universitetets computerklynge, han var fascineret, fordi problemet kunne oversættes, ved hjælp af diskret grafteori, til en form, som computere kunne udforske. I denne form, kaldet en Keller-graf, forskere kunne søge efter "kliker" - undergrupper af elementer, der forbinder uden at dele et ansigt, dermed afkræfter formodningen.

I 2002 Mackey gjorde netop det, opdager en klike i dimension otte. Ved at gøre det, han beviste, at formodningen fejler i den dimension, og, i forlængelse heraf, i dimension ni.

Det efterlod formodningen uafklaret for dimension syv.

Da Heule ankom til CMU fra University of Texas sidste år, han havde allerede et ry for at bruge SAT-løseren til at løse langvarige åbne matematikproblemer.

"Jeg tænkte ved mig selv, måske vi kan bruge hans teknik, " huskede Mackey. Inden længe, han begyndte at diskutere, hvordan man bruger SAT-løseren på Kellers formodning med Heule og Joshua Brakensiek, en dobbelt hovedfag i matematiske videnskaber og datalogi, der nu er i gang med en ph.d. i datalogi ved Stanford University.

En SAT-løser kræver strukturering af problemet ved hjælp af en propositionsformel - (A eller ikke B) og (B eller C), osv. — så løseren kan undersøge alle de mulige variable for kombinationer, der vil opfylde alle betingelserne.

"Der er mange måder at lave disse oversættelser på, og kvaliteten af ​​oversættelsen gør eller ødelægger typisk din evne til at løse problemet, " sagde Heule.

Med 15 års erfaring, Heule er dygtig til at udføre disse oversættelser. Et af hans forskningsmål er at udvikle automatiseret ræsonnement, så denne oversættelse kan udføres automatisk, giver flere mennesker mulighed for at bruge disse værktøjer på deres problemer.

Selv med en oversættelse af høj kvalitet, antallet af kombinationer, der skulle kontrolleres i dimension syv, var forbløffende - et tal med 324 cifre - med en løsning, der ikke var i syne, selv med en supercomputer. Men Heule og de andre brugte en række tricks for at reducere problemets størrelse. For eksempel, hvis en datakonfiguration viste sig ubrugelig, de kunne automatisk afvise andre kombinationer, der var afhængige af det. Og da meget af dataene var symmetriske, programmet kunne udelukke spejlbilleder af en konfiguration, hvis den nåede en blindgyde i ét arrangement.

Ved at bruge disse teknikker, de reducerede deres søgning til omkring en milliard konfigurationer. De fik følgeskab i denne indsats af David Narvaez, en ph.d. studerende ved Rochester Institute of Technology, som var gæsteforsker i efteråret 2019.

Når de kørte deres kode på en klynge af 40 computere, de havde endelig et svar:formodningen er sand i dimension syv.

"Grunden til, at vi lykkedes, er, at John har årtiers erfaring og indsigt i dette problem, og vi var i stand til at transformere det til en computergenereret søgning, " sagde Heule.

Beviset for resultatet beregnes fuldt ud af computeren, Heule sagde, i modsætning til mange publikationer, der kombinerer computerkontrollerede dele af et korrektur med manuelle opskrivninger af andre dele. Det gør det svært for læserne at forstå, bemærkede han. Computerbeviset til Keller-løsningen inkluderer alle aspekter af løsningen, inklusive en symmetri-brydende del bidraget af Narvaez, Heule understregede, så intet aspekt af beviset behøver at stole på manuel indsats.

"Vi kan have reel tillid til rigtigheden af ​​dette resultat, " sagde han. Et papir, der beskriver beslutningen af ​​Heule, Mackey, Brakensiek og Narvaez vandt en pris for bedste papir ved den internationale fælles konference om automatiseret ræsonnement i juni.

Løsning af Kellers formodning har praktiske anvendelser, sagde Mackey. De kliker, som videnskabsmænd leder efter for at modbevise formodningen, er nyttige til at generere ikke-lineære koder, der kan gøre transmissionen af ​​data hurtigere. SAT-løseren kan således bruges til at finde højere dimensionelle ikke-lineære koder end tidligere muligt.

Heule foreslog for nylig at bruge SAT-løseren til at tackle et endnu mere berømt matematisk problem:Collatz-formodningen. I dette problem, ideen er at vælge ethvert positivt helt tal og dividere med 2, hvis det er et lige tal, eller gange med 3 og tilføje 1, hvis det er et ulige tal. Anvend derefter de samme regler for det resulterende tal og hvert efterfølgende resultat. Formodningen er, at det endelige resultat altid vil være 1.

At løse Collatz med SAT-løseren "er et langt skud, " Erkendte Heule. Men det er et aspirationsmål, han tilføjede, forklarer, at SAT-løseren kan bruges til at løse en række mindre skræmmende matematiske problemer, selvom Collatz viser sig uopnåelig.