Carnegie Mellon University datavetare och matematiker har löst det sista, envis del av Kellers gissningar, ett geometriproblem som forskare har förbryllat i 90 år.

Genom att strukturera pusslet som vad datavetare kallar ett tillfredsställelseproblem, forskarna slapp problemet med fyra månaders frenesierad datorprogrammering och bara 30 minuters beräkning med ett kluster av datorer.

"Jag blev verkligen glad när vi löste det, men sedan blev jag lite ledsen över att problemet var borta, sa John Mackey, en lärarprofessor vid datavetenskapsavdelningen (CSD) och institutionen för matematiska vetenskaper som hade fullföljt Kellers gissningar sedan han var doktorand för 30 år sedan. "Men så kände jag mig glad igen. Det är bara den här känslan av tillfredsställelse."

Lösningen var ännu en framgång för ett tillvägagångssätt pionjärt av Marijn Heule, en docent i datavetenskap som började på CSD i augusti förra året. Heule har använt en SAT-lösare – ett datorprogram som använder propositionell logik för att lösa tillfredsställbarhetsproblem (SAT) – för att övervinna flera grymma matematiska utmaningar, inklusive Pythagoras trippelproblem och Schur nummer 5.

"Problemet har fascinerat många människor i decennier, nästan ett sekel, " Sa Heule om Kellers gissningar. "Detta är verkligen ett skyltfönster för vad som kan göras nu som inte var möjligt tidigare."

Gissningen, poserad av den tyske matematikern Eduard Ott-Heinrich Keller, har med kakel att göra – specifikt, hur man täcker ett område med lika stora plattor utan några luckor eller överlappning. Gissningen är att minst två av brickorna måste dela en kant och att detta är sant för utrymmen av alla dimensioner.

Det är lätt att bevisa att det är sant för tvådimensionella brickor och tredimensionella kuber. Från och med 1940, gissningarna hade visat sig vara sanna för alla dimensioner upp till sex. 1990, dock, matematiker bevisade att det inte fungerar vid dimension 10 eller högre.

Det var då Kellers gissningar fångade Mackeys fantasi, sedan student vid University of Hawaii. Med ett kontor intill universitetets datorkluster, han var fascinerad eftersom problemet kunde översättas, använda diskret grafteori, till en form som datorer kan utforska. I denna form, kallas en Keller-graf, forskare kunde söka efter "klickar" - delmängder av element som ansluter utan att dela ett ansikte, motbevisar alltså gissningen.

År 2002, Mackey gjorde just det, upptäcka en klick i dimension åtta. Genom att göra så, han bevisade att gissningarna misslyckas i den dimensionen och, i förlängningen, i dimension nio.

Det lämnade gissningarna olösta för dimension sju.

När Heule anlände till CMU från University of Texas förra året, han hade redan ett rykte om sig att använda SAT-lösaren för att lösa långvariga öppna matematiska problem.

"Jag tänkte för mig själv, kanske vi kan använda hans teknik, "mindes Mackey. Snart han började diskutera hur man använder SAT-lösaren på Kellers gissning med Heule och Joshua Brakensiek, en dubbel major i matematiska vetenskaper och datavetenskap som nu tar en doktorsexamen. i datavetenskap vid Stanford University.

En SAT-lösare kräver strukturering av problemet med hjälp av en propositionsformel - (A eller inte B) och (B eller C), etc. — så att lösaren kan undersöka alla möjliga variabler för kombinationer som kommer att uppfylla alla villkor.

"Det finns många sätt att göra dessa översättningar, och kvaliteten på översättningen gör eller bryter vanligtvis din förmåga att lösa problemet, sa Heule.

Med 15 års erfarenhet, Heule är skicklig på att utföra dessa översättningar. Ett av hans forskningsmål är att utveckla automatiserade resonemang så att denna översättning kan göras automatiskt, låta fler människor använda dessa verktyg på sina problem.

Även med en översättning av hög kvalitet, antalet kombinationer som skulle kontrolleras i dimension sju var häpnadsväckande – ett tal med 324 siffror – med en lösning ingenstans i sikte ens med en superdator. Men Heule och de andra använde ett antal knep för att minska storleken på problemet. Till exempel, om en datakonfiguration visade sig olämplig, de kunde automatiskt förkasta andra kombinationer som förlitade sig på det. Och eftersom mycket av datan var symmetrisk, programmet skulle kunna utesluta spegelbilder av en konfiguration om den nådde en återvändsgränd i ett arrangemang.

Genom att använda dessa tekniker, de minskade sin sökning till ungefär en miljard konfigurationer. De fick sällskap i denna ansträngning av David Narvaez, en Ph.D. student vid Rochester Institute of Technology, som var gästforskare hösten 2019.

När de väl körde sin kod på ett kluster med 40 datorer, de fick till slut ett svar:gissningarna är sanna i dimension sju.

"Anledningen till att vi lyckades är att John har decennier av erfarenhet och insikt i detta problem och vi kunde omvandla det till en datorgenererad sökning, sa Heule.

Beviset på resultatet beräknas helt av datorn, Heule sa, i motsats till många publikationer som kombinerar datorkontrollerade delar av ett korrektur med manuella uppskrivningar av andra delar. Det gör det svårt för läsarna att förstå, noterade han. Datorbeviset för Keller-lösningen inkluderar alla aspekter av lösningen, inklusive en symmetribrytande del från Narvaez, Heule betonade, så att ingen aspekt av beviset behöver förlita sig på manuell ansträngning.

"Vi kan ha verkligt förtroende för riktigheten av detta resultat, " sa han. Ett papper som beskriver resolutionen av Heule, Mackey, Brakensiek och Narvaez vann ett pris för bästa papper vid den internationella gemensamma konferensen om automatiserat resonemang i juni.

Att lösa Kellers gissningar har praktiska tillämpningar, sa Mackey. De klick som forskare letar efter för att motbevisa gissningarna är användbara för att generera olinjära koder som kan göra överföringen av data snabbare. SAT-lösaren kan således användas för att hitta icke-linjära koder med högre dimension än vad som tidigare varit möjligt.

Heule föreslog nyligen att man skulle använda SAT-lösaren för att ta itu med ett ännu mer känt matematiskt problem:Collatz-förmodan. I detta problem, Tanken är att välja ett positivt heltal och dividera med 2 om det är ett jämnt tal eller multiplicera med 3 och lägga till 1 om det är ett udda tal. Tillämpa sedan samma regler på det resulterande numret och varje efterföljande resultat. Gissningen är att det slutliga resultatet alltid kommer att vara 1.

Att lösa Collatz med SAT-lösaren "är ett långt försök, " erkände Heule. Men det är ett ambitiöst mål, han lade till, förklarar att SAT-lösaren kan användas för att lösa ett antal mindre skrämmande matematiska problem även om Collatz visar sig ouppnåeligt.