Siffran 15 beskriver den hemliga gränsen för ett oändligt rutnät

Som doktorand vid University of Chile, Bernardo Subercaseaux tog en svag syn på att använda datorer för att göra matematik. Det verkade strida mot verklig intellektuell upptäckt.

"Det finns en instinkt eller magreaktion mot att använda datorer för att lösa dina problem, som att det går emot den idealiska skönheten eller elegansen i ett fantastiskt argument", sa han.

Men så 2020 blev Subercaseaux kär, och som ofta händer ändrades hans prioriteringar. Objektet för hans besatthet var en fråga som han såg på ett onlineforum. De flesta problemen skannade han och glömde, men detta fångade hans blick. Han svepte åt höger.

"Det första jag gjorde var att gilla inlägget i Facebook-gruppen, i hopp om att få ett meddelande senare när någon annan postade en lösning", sa han.

Frågan handlade om att fylla ett oändligt rutnät med siffror. Det var inte, som det visade sig, den typ av problem man löser på en lärka. För att kunna göra det var Subercaseaux tvungen att lämna Chile för forskarskola vid Carnegie Mellon University.

Där, i augusti 2021, hade han ett slumpmässigt möte med Marijn Heule, en datavetare som använder enorm datorkraft för att lösa svåra matematikfrågor. Subercaseaux frågade Heule om han ville försöka sig på problemet, och startade ett samarbete som kulminerade i januari i ett bevis som kan summeras med ett enda tal: 15.

Alla möjliga sätt

2002, Wayne Goddard från Clemson University och några likasinnade matematiker höll på med problem i kombinatorik och försökte komma på nya vändningar på fältets grundfrågor om färgläggning av kartor med tanke på vissa begränsningar.

Så småningom landade de på ett problem som börjar med ett rutnät, som ett ark rutat papper som pågår för evigt. Målet är att fylla den med siffror. Det finns bara en begränsning: Avståndet mellan varje förekomst av samma nummer måste vara större än själva talet. (Avståndet mäts genom att lägga samman den vertikala och horisontella separationen, ett mått som kallas "taxibil"-avstånd för hur det liknar att röra sig på rutnät i stadsgator.) Ett par 1:or kan inte uppta angränsande celler, som har ett taxiavstånd på 1, men de kan placeras i direkt diagonala celler, som har ett avstånd på 2.

Till en början ville Goddard och hans medarbetare veta om det ens var möjligt att fylla ett oändligt rutnät med en ändlig uppsättning siffror. Men vid tiden han och hans fyra medarbetare publicerade detta "packningsfärgningsproblem". i tidskriften Ars Combinatoria 2008 hade de bevisat att det går att lösa med 22 nummer. De visste också att det inte fanns något sätt att lösa det med bara fem siffror. Det innebar att det faktiska svaret på problemet - det minsta antalet siffror som behövs - låg någonstans däremellan.

Forskarna fyllde faktiskt inte ett oändligt rutnät. De behövde inte. Istället räcker det att ta en liten delmängd av rutnätet - säg en 10 x 10 kvadrat - fyll den med siffror och visa sedan att kopior av den ifyllda delmängden kan placeras bredvid varandra, som du skulle täcka en golv med kopior av ett kakel.

När Subercaseaux först fick reda på problemet började han leta efter brickor med penna och papper. Han skulle skissa rutnät med siffror, stryka över dem, försöka igen. Han tröttnade snart på det tillvägagångssättet, och han bad en vän att designa ett webbaserat verktyg som liknade spelet Minesweeper och gjorde det möjligt för honom att testa kombinationer snabbare. Efter ytterligare några veckors arbete hade han övertygat sig själv om att det inte fanns något sätt att packa ett rutnät med åtta nummer, men han kunde inte komma längre än så - det fanns alldeles för många potentiella former som brickorna kunde ta och för många på olika sätt kan de fyllas med siffror.

Problemet, som senare skulle bli tydligt, är att det är mycket svårare att visa att rutnätet inte kan täckas av en viss uppsättning siffror än att visa att det kan. "Det är inte bara att visa att ett sätt inte fungerar, det är att visa att alla möjliga sätt inte fungerar," sa Goddard.

Efter att Subercaseaux började på CMU och övertygade Heule att arbeta med honom, hittade de snabbt ett sätt att täcka rutnätet med 15 nummer. De kunde också utesluta möjligheten att lösa problemet med endast 12 nummer. Men deras känslor av triumf var kortlivade, eftersom de insåg att de bara hade återgett resultat som hade funnits länge: Så långt tillbaka som 2017 hade forskare vetat att svaret inte var mindre än 13 eller större än 15 .

För en förstaårsstudent som hade lockat en storprofessor att arbeta med sitt husdjursproblem, var det en oroande upptäckt. "Jag blev förskräckt. Jag hade i princip arbetat i flera månader med ett problem utan att inse detta, och ännu värre, jag hade gjort Marijn slösa bort sin tid på det!" Subercaseaux skrev i ett blogginlägg som sammanfattar deras arbete.

Heule fann dock upptäckten av tidigare resultat uppfriskande. Det visade att andra forskare fann problemet viktigt nog att arbeta med, och bekräftade för honom att det enda resultat som var värt att få var att lösa problemet helt.

"När vi väl insåg att det hade varit 20 års arbete med problemet, förändrade det bilden helt", sa han.

Undviker det vulgära

Under åren hade Heule gjort en karriär av att hitta effektiva sätt att söka bland enorma möjliga kombinationer. Hans tillvägagångssätt kallas SAT-lösning - en förkortning för "satisfiability". Det innebär att konstruera en lång formel, kallad en boolesk formel, som kan ha två möjliga resultat: 0 eller 1. Om resultatet är 1 är formeln sann och problemet är tillfredsställt.

För packningsfärgningsproblemet kan varje variabel i formeln representera om en given cell är upptagen av ett givet nummer. En dator letar efter sätt att tilldela variabler för att uppfylla formeln. Om datorn kan göra det vet du att det är möjligt att packa rutnätet under de villkor du har ställt in.

Tyvärr kan en enkel kodning av packningsfärgningsproblemet som en boolesk formel sträcka sig till många miljoner termer - en dator, eller till och med en flotta av datorer, skulle kunna köra för evigt och testa alla olika sätt att tilldela variabler inom den.

"Att försöka göra den här brutala kraften skulle ta tills universum slutar om du gjorde det naivt," sa Goddard. "Så du behöver några coola förenklingar för att få ner det till något som till och med är möjligt."

Dessutom, varje gång du lägger till ett nummer i packningsfärgproblemet blir det cirka 100 gånger svårare, på grund av hur de möjliga kombinationerna multipliceras. Detta innebär att om en bank av datorer som arbetar parallellt kunde utesluta 12 på en enda dag av beräkning, skulle de behöva 100 dagars beräkningstid för att utesluta 13.

Heule och Subercaseaux ansåg att skala upp en brute-force beräkningsmetod som vulgär, på ett sätt. "Vi hade flera lovande idéer, så vi tog tankesättet "Låt oss försöka optimera vårt tillvägagångssätt tills vi kan lösa det här problemet på mindre än 48 timmars beräkning i klustret", sa Subercaseaux.

För att göra det var de tvungna att komma på sätt att begränsa antalet kombinationer som datorklustret var tvungen att prova.

"[De] vill inte bara lösa det, utan lösa det på ett imponerande sätt," sa Alexander Soifer vid University of Colorado, Colorado Springs.

Heule och Subercaseaux insåg att många kombinationer i huvudsak är desamma. Om du försöker fylla en rombformad bricka med åtta olika siffror, spelar det ingen roll om det första siffran du placerar är en upp och en till höger om mittrutan, eller en ner och en till vänster om mitttorget. De två placeringarna är symmetriska med varandra och begränsar ditt nästa drag på exakt samma sätt, så det finns ingen anledning att kontrollera dem båda.

Heule och Subercaseaux lade till regler som gjorde att datorn kunde behandla symmetriska kombinationer som likvärdiga, vilket minskade den totala söktiden med en faktor åtta. De använde också en teknik som Heule hade utvecklat i tidigare arbete som kallas kub och erövra, vilket gjorde att de kunde testa fler kombinationer parallellt med varandra. Om du vet att en given cell måste innehålla antingen 3, 5 eller 7, kan du dela upp problemet och testa var och en av de tre möjligheterna samtidigt på olika uppsättningar av datorer.

I januari 2022 gjorde dessa förbättringar det möjligt för Heule och Subercaseaux att utesluta 13 som svaret på packningsfärgningsproblemet i ett experiment som krävde mindre än två dagars beräkningstid. Detta lämnade dem med två möjliga svar: 14 eller 15.

Ett stort plus

För att utesluta 14 – och lösa problemet – var Heule och Subercaseaux tvungna att hitta ytterligare sätt att påskynda datorsökningen.

Till en början hade de skrivit en boolesk formel som tilldelade variabler till varje enskild cell i rutnätet. Men i september 2022 insåg de att de inte behövde gå vidare på cell-för-cell-basis. Istället upptäckte de att det var mer effektivt att överväga små regioner som består av fem celler i form av ett plustecken.

De skrev om sin booleska formel så att flera variabler representerade frågor som: Finns det en 7:a någonstans inom denna plusformade region? Datorn behövde inte identifiera exakt var i regionen 7:an kan befinna sig. Det behövde bara avgöra om det fanns där eller inte - en fråga som kräver betydligt färre beräkningsresurser att svara på.

"Att ha variabler som bara talar om plusser istället för specifika platser visade sig vara mycket bättre än att prata om dem i specifika celler," sa Heule.

Med hjälp av effektiviteten i plussökningen uteslöt Heule och Subercaseaux 14 i ett datorexperiment i november 2022 som slutade med att det tog mindre tid att köra än det de hade använt för att utesluta 13. De ägnade de kommande fyra månaderna åt att verifiera att datorns slutsats var korrekt – nästan lika mycket tid som de hade ägnat åt att göra det möjligt för datorn att komma fram till den slutsatsen från början.

"Det var glädjande att tänka på att det vi hade skapat som en slags sidofråga i någon slumpmässig journal hade fått grupper av människor att spendera, som det visade sig, månader av sin tid på att försöka komma på hur de skulle lösa det," Goddard sa.

För Subercaseaux var det den första riktiga triumfen i hans forskarkarriär. Och även om det kanske inte var den typ av upptäckt han hade idealiserat när han först övervägde att arbeta i matematik, fann han att det i slutändan hade sina egna intellektuella belöningar.

"Det är inte att förstå formuläret där du ger mig en svart tavla och jag kan visa dig varför det är 15," sa han. "Men vi har fått förståelse för hur problemets begränsningar fungerar, hur mycket bättre det är att ha en 6 här eller en 7:a där. Vi har fått mycket intuitiv förståelse.”