Gli informatici e i matematici della Carnegie Mellon University hanno risolto l'ultimo, pezzo ostinato della congettura di Keller, un problema di geometria su cui gli scienziati si sono interrogati per 90 anni.

Strutturando il puzzle come quello che gli informatici chiamano problema di soddisfacibilità, i ricercatori hanno risolto il problema con quattro mesi di frenetica programmazione di computer e appena 30 minuti di calcolo utilizzando un cluster di computer.

"Ero davvero felice quando l'abbiamo risolto, ma poi ero un po' triste che il problema fosse sparito, " disse John Mackey, un professore del Dipartimento di Informatica (CSD) e del Dipartimento di Scienze Matematiche che aveva perseguito la congettura di Keller da quando era uno studente laureato 30 anni fa. "Ma poi mi sono sentito di nuovo felice. C'è solo questa sensazione di soddisfazione".

La soluzione è stata l'ennesimo successo per un approccio sperimentato da Marijn Heule, un professore associato di informatica entrato a far parte del CSD lo scorso agosto. Heule ha utilizzato un risolutore SAT, un programma per computer che utilizza la logica proposizionale per risolvere problemi di soddisfacibilità (SAT) per superare diverse sfide matematiche, compreso il problema delle triple pitagoriche e il numero di Schur 5.

"Il problema ha incuriosito molte persone per decenni, quasi un secolo, " Heule ha detto della congettura di Keller. "Questa è davvero una vetrina per ciò che può essere fatto ora che non era possibile in precedenza".

La congettura, poste dal matematico tedesco Eduard Ott-Heinrich Keller, ha a che fare con la piastrellatura, in particolare, come coprire un'area con piastrelle di uguali dimensioni senza spazi o sovrapposizioni. La congettura è che almeno due delle tessere dovranno condividere un bordo e che questo sia vero per spazi di ogni dimensione.

È facile dimostrare che è vero per tessere bidimensionali e cubi tridimensionali. A partire dal 1940, la congettura si era dimostrata vera per tutte le dimensioni fino a sei. Nel 1990, però, i matematici hanno dimostrato che non funziona a dimensione 10 o superiore.

Fu allora che la congettura di Keller catturò l'immaginazione di Mackey, poi uno studente all'Università delle Hawaii. Con un ufficio vicino al cluster di elaborazione dell'università, era incuriosito perché il problema poteva essere tradotto, usando la teoria dei grafi discreti, in una forma che i computer potrebbero esplorare. In questa forma, chiamato grafico di Keller, i ricercatori potrebbero cercare "cricche", sottoinsiemi di elementi che si connettono senza condividere un volto, smentendo così la congettura.

Nel 2002, Mackey ha fatto proprio questo, scoprendo una cricca in dimensione otto. Facendo così, ha dimostrato che la congettura fallisce a quella dimensione e, per estensione, nella dimensione nove.

Ciò ha lasciato la congettura irrisolta per la dimensione sette.

Quando Heule è arrivato alla CMU dall'Università del Texas l'anno scorso, aveva già la reputazione di utilizzare il risolutore SAT per risolvere problemi di matematica aperti di vecchia data.

"Ho pensato, forse possiamo usare la sua tecnica, "Ricordò Mackey. In poco tempo, iniziò a discutere su come usare il risolutore SAT sulla congettura di Keller con Heule e Joshua Brakensiek, una doppia specializzazione in scienze matematiche e informatica che ora sta perseguendo un dottorato di ricerca. in informatica alla Stanford University.

Un risolutore SAT richiede la strutturazione del problema utilizzando una formula proposizionale:(A o non B) e (B o C), ecc. - in modo che il risolutore possa esaminare tutte le possibili variabili per le combinazioni che soddisferanno tutte le condizioni.

"Ci sono molti modi per fare queste traduzioni, e la qualità della traduzione in genere crea o interrompe la tua capacità di risolvere il problema, " ha detto Heule.

Con 15 anni di esperienza, Heule è abile nell'eseguire queste traduzioni. Uno dei suoi obiettivi di ricerca è sviluppare un ragionamento automatizzato in modo che questa traduzione possa essere eseguita automaticamente, consentendo a più persone di utilizzare questi strumenti per i loro problemi.

Anche con una traduzione di alta qualità, il numero di combinazioni da controllare nella dimensione sette era sbalorditivo - un numero con 324 cifre - con una soluzione che non si vedeva nemmeno con un supercomputer. Ma Heule e gli altri hanno applicato una serie di trucchi per ridurre le dimensioni del problema. Ad esempio, se una configurazione dei dati si è rivelata inattuabile, potevano rifiutare automaticamente altre combinazioni che si basavano su di esso. E poiché gran parte dei dati era simmetrica, il programma potrebbe escludere le immagini speculari di una configurazione se raggiungesse un vicolo cieco in una disposizione.

Utilizzando queste tecniche, hanno ridotto la loro ricerca a circa un miliardo di configurazioni. A loro si unirono in questo sforzo David Narvaez, un dottorato di ricerca studente al Rochester Institute of Technology, che era un ricercatore in visita nell'autunno del 2019.

Una volta eseguito il codice su un cluster di 40 computer, finalmente hanno avuto una risposta:la congettura è vera nella dimensione sette.

"Il motivo per cui ci siamo riusciti è che John ha decenni di esperienza e conoscenza di questo problema e siamo stati in grado di trasformarlo in una ricerca generata dal computer, " ha detto Heule.

La dimostrazione del risultato è completamente calcolata dal computer, Heule ha detto, a differenza di molte pubblicazioni che combinano parti di una bozza controllate dal computer con riscritture manuali di altre parti. Ciò rende difficile la comprensione per i lettori, ha notato. La prova del computer per la soluzione Keller include tutti gli aspetti della soluzione, inclusa una porzione di rottura della simmetria fornita da Narvaez, Heule ha sottolineato, in modo che nessun aspetto della dimostrazione debba fare affidamento su uno sforzo manuale.

"Possiamo avere vera fiducia nella correttezza di questo risultato, " ha detto. Un documento che descrive la risoluzione di Heule, Macchi, Brakensiek e Narvaez hanno vinto il premio Best Paper alla International Joint Conference on Automated Reasoning a giugno.

Risolvere la congettura di Keller ha applicazioni pratiche, disse Mackey. Quelle cricche che gli scienziati cercano per confutare la congettura sono utili per generare codici non lineari che possono rendere più veloce la trasmissione dei dati. Il risolutore SAT quindi può essere utilizzato per trovare codici non lineari dimensionali più elevati rispetto a quanto precedentemente possibile.

Heule ha recentemente proposto di utilizzare il risolutore SAT per affrontare un problema matematico ancora più famoso:la congettura di Collatz. In questo problema, l'idea è di scegliere un qualsiasi numero intero positivo e dividere per 2 se è un numero pari o moltiplicare per 3 e aggiungere 1 se è un numero dispari. Quindi applica le stesse regole al numero risultante e a ogni risultato successivo. La congettura è che il risultato finale sarà sempre 1.

Risolvere Collatz con il risolutore SAT "è un'impresa ardua, " Heule ha riconosciuto. Ma è un obiettivo ambizioso, Ha aggiunto, spiegando che il risolutore SAT potrebbe essere utilizzato per risolvere una serie di problemi matematici meno intimidatori anche se Collatz si dimostrasse irraggiungibile.