Computerwetenschappers en wiskundigen van de Carnegie Mellon University hebben de laatste, koppig stuk van Keller's vermoeden, een meetkundig probleem waar wetenschappers al 90 jaar over puzzelen.

Door de puzzel te structureren als wat computerwetenschappers een verzadigingsprobleem noemen, de onderzoekers losten het probleem op met vier maanden waanzinnig computerprogrammeren en slechts 30 minuten rekenen met behulp van een cluster van computers.

"Ik was heel blij toen we het hadden opgelost, maar toen was ik een beetje verdrietig dat het probleem weg was, " zei John Mackey, een onderwijsprofessor in de Computer Science Department (CSD) en Department of Mathematical Sciences die Keller's vermoeden had nagestreefd sinds hij 30 jaar geleden een afgestudeerde student was. "Maar toen voelde ik me weer gelukkig. Er is gewoon een gevoel van voldoening."

De oplossing was wederom een ​​succes voor een door Marijn Heule gepionierde aanpak, een universitair hoofddocent computerwetenschappen die afgelopen augustus bij CSD kwam. Heule heeft een SAT-oplosser gebruikt - een computerprogramma dat propositielogica gebruikt om verzadigingsproblemen (SAT) op te lossen - om verschillende grijze wiskundige uitdagingen te overwinnen, inclusief het Pythagoras triples-probleem en Schur nummer 5.

"Het probleem intrigeert veel mensen al tientallen jaren, bijna een eeuw, Heule zei over het vermoeden van Keller. "Dit is echt een etalage voor wat nu kan wat voorheen niet mogelijk was."

het vermoeden, gesteld door de Duitse wiskundige Eduard Ott-Heinrich Keller, heeft te maken met tegels, in het bijzonder hoe een gebied te bedekken met tegels van gelijke grootte zonder gaten of overlap. Het vermoeden is dat ten minste twee van de tegels een rand zullen moeten delen en dat dit geldt voor ruimtes van elke dimensie.

Het is gemakkelijk te bewijzen dat het waar is voor tweedimensionale tegels en driedimensionale kubussen. Vanaf 1940, het vermoeden was bewezen waar voor alle dimensies tot zes. In 1990, echter, wiskundigen bewezen dat het niet werkt op dimensie 10 of hoger.

Toen sprak het vermoeden van Keller tot de verbeelding van Mackey, dan een student aan de Universiteit van Hawaï. Met een kantoor naast het rekencluster van de universiteit, hij was geïntrigeerd omdat het probleem vertaald kon worden, met behulp van discrete grafentheorie, in een vorm die computers kunnen verkennen. In deze vorm, een Keller-grafiek genoemd, onderzoekers konden zoeken naar 'kliekjes' - subsets van elementen die met elkaar verbonden zijn zonder een gezicht te delen, waardoor het vermoeden wordt weerlegd.

In 2002, Mackey deed precies dat, het ontdekken van een kliek in dimensie acht. Door het zo te doen, hij bewees dat het vermoeden faalt op die dimensie en, door verlenging, in dimensie negen.

Dat liet het vermoeden onopgelost voor dimensie zeven.

Toen Heule vorig jaar aankwam bij CMU van de Universiteit van Texas, hij had al een reputatie voor het gebruik van de SAT-oplosser om al lang bestaande open wiskundige problemen op te lossen.

"Ik bedacht me, misschien kunnen we zijn techniek gebruiken, " herinnerde Mackey zich. Het duurde niet lang, hij begon met Heule en Joshua Brakensiek te bespreken hoe hij de SAT-oplosser op het vermoeden van Keller kon gebruiken, een dubbele major in wiskundige wetenschappen en informatica die nu een Ph.D. in computerwetenschappen aan de Stanford University.

Een SAT-oplosser vereist het structureren van het probleem met behulp van een propositieformule - (A of niet B) en (B of C), enz. - zodat de oplosser alle mogelijke variabelen kan onderzoeken op combinaties die aan alle voorwaarden voldoen.

"Er zijn veel manieren om deze vertalingen te maken, en de kwaliteit van de vertaling maakt of breekt doorgaans uw vermogen om het probleem op te lossen, ' zei Heule.

Met 15 jaar ervaring, Heule is bedreven in het uitvoeren van deze vertalingen. Een van zijn onderzoeksdoelen is om geautomatiseerd redeneren te ontwikkelen, zodat deze vertaling automatisch kan worden gedaan, waardoor meer mensen deze tools kunnen gebruiken voor hun problemen.

Zelfs met een vertaling van hoge kwaliteit, het aantal combinaties dat moest worden gecontroleerd in dimensie zeven was verbijsterend - een getal met 324 cijfers - met een oplossing die zelfs met een supercomputer nergens in zicht was. Maar Heule en de anderen pasten een aantal trucjes toe om het probleem te verkleinen. Bijvoorbeeld, als één dataconfiguratie onwerkbaar bleek, ze konden automatisch andere combinaties afwijzen die erop vertrouwden. En aangezien veel van de gegevens symmetrisch waren, het programma zou spiegelbeelden van een configuratie kunnen uitsluiten als het in een opstelling doodloopt.

Met behulp van deze technieken, ze brachten hun zoektocht terug tot ongeveer een miljard configuraties. Ze werden bij deze inspanning vergezeld door David Narvaez, een doctoraat student aan het Rochester Institute of Technology, die in het najaar van 2019 gastonderzoeker was.

Toen ze hun code eenmaal op een cluster van 40 computers hadden uitgevoerd, ze hadden eindelijk een antwoord:het vermoeden is waar in dimensie zeven.

"De reden dat het ons is gelukt, is dat John tientallen jaren ervaring en inzicht heeft in dit probleem en dat we het hebben kunnen omzetten in een door de computer gegenereerde zoekopdracht, ' zei Heule.

Het bewijs van de uitslag wordt volledig door de computer berekend, Heule zei, in tegenstelling tot veel publicaties die computergestuurde delen van een proef combineren met handmatige opschrijvingen van andere delen. Dat maakt het moeilijk voor lezers om te begrijpen, hij merkte. De computerproef voor de Keller-oplossing omvat alle aspecten van de oplossing, inclusief een symmetrie-brekend deel bijgedragen door Narvaez, Heule benadrukte, zodat geen enkel aspect van het bewijs hoeft te vertrouwen op handmatige inspanning.

"We kunnen echt vertrouwen hebben in de juistheid van dit resultaat, " zei hij. Een paper waarin de resolutie van Heule wordt beschreven, Mackey, Brakensiek en Narvaez wonnen een Best Paper award op de International Joint Conference on Automated Reasoning in juni.

Het oplossen van het vermoeden van Keller heeft praktische toepassingen, zei Mackey. Die kliekjes waar wetenschappers naar op zoek zijn om het vermoeden te weerleggen, zijn nuttig bij het genereren van niet-lineaire codes die de overdracht van gegevens sneller kunnen maken. De SAT-oplosser kan dus worden gebruikt om niet-lineaire codes met een hogere dimensie te vinden dan voorheen mogelijk was.

Heule stelde onlangs voor om de SAT-oplosser te gebruiken om een ​​nog beroemder wiskundig probleem aan te pakken:het vermoeden van Collatz. Bij dit probleem het idee is om een ​​willekeurig positief geheel getal te kiezen en te delen door 2 als het een even getal is of te vermenigvuldigen met 3 en 1 op te tellen als het een oneven getal is. Pas vervolgens dezelfde regels toe op het resulterende getal en elk opeenvolgend resultaat. Het vermoeden is dat het uiteindelijke resultaat altijd 1 zal zijn.

Collatz oplossen met de SAT-oplosser "is een schot in de roos, " erkende Heule. Maar het is een ambitieus doel, hij voegde toe, waarin wordt uitgelegd dat de SAT-oplosser kan worden gebruikt om een ​​aantal minder intimiderende wiskundige problemen op te lossen, zelfs als Collatz onbereikbaar blijkt te zijn.