Les informaticiens et les mathématiciens de l'Université Carnegie Mellon ont résolu le dernier, morceau têtu de la conjecture de Keller, un problème de géométrie sur lequel les scientifiques s'interrogent depuis 90 ans.

En structurant le puzzle comme ce que les informaticiens appellent un problème de satisfiabilité, les chercheurs ont résolu le problème avec quatre mois de programmation informatique frénétique et seulement 30 minutes de calcul à l'aide d'un groupe d'ordinateurs.

"J'étais vraiment heureux quand nous l'avons résolu, mais ensuite j'étais un peu triste que le problème ait disparu, " dit John Mackey, un professeur enseignant au Département d'informatique (CSD) et au Département des sciences mathématiques qui avait poursuivi la conjecture de Keller depuis qu'il était un étudiant diplômé il y a 30 ans. "Mais ensuite je me suis senti à nouveau heureux. Il y a juste ce sentiment de satisfaction."

La solution a été un nouveau succès pour une approche initiée par Marijn Heule, professeur agrégé d'informatique qui a rejoint le CSD en août dernier. Heule a utilisé un solveur SAT - un programme informatique qui utilise la logique propositionnelle pour résoudre des problèmes de satisfaisabilité (SAT) - pour relever plusieurs défis mathématiques anciens, y compris le problème des triplets de Pythagore et le nombre de Schur 5.

"Le problème a intrigué beaucoup de gens pendant des décennies, près d'un siècle, " Heule a dit de la conjecture de Keller. " C'est vraiment une vitrine pour ce qui peut être fait maintenant qui n'était pas possible auparavant. "

La conjecture, posée par le mathématicien allemand Eduard Ott-Heinrich Keller, a à voir avec le carrelage - en particulier, comment couvrir une zone avec des carreaux de taille égale sans aucun espace ni chevauchement. La conjecture est qu'au moins deux des tuiles devront partager un bord et que cela est vrai pour les espaces de toutes les dimensions.

Il est facile de prouver que c'est vrai pour les tuiles bidimensionnelles et les cubes tridimensionnels. A partir de 1940, la conjecture s'était avérée vraie pour toutes les dimensions jusqu'à six. En 1990, cependant, les mathématiciens ont prouvé que cela ne fonctionne pas à la dimension 10 ou au-dessus.

C'est alors que la conjecture de Keller a capturé l'imagination de Mackey, puis étudiant à l'Université d'Hawaï. Avec un bureau à côté du cluster de calcul de l'université, il était intrigué car le problème pouvait être traduit, en utilisant la théorie des graphes discrets, sous une forme que les ordinateurs pourraient explorer. Sous cette forme, appelé graphe de Keller, les chercheurs pourraient rechercher des "cliques" - des sous-ensembles d'éléments qui se connectent sans partager de visage, réfutant ainsi la conjecture.

En 2002, Mackey a fait exactement cela, découvrir une clique en dimension huit. En faisant cela, il a prouvé que la conjecture échoue à cette dimension et, par extension, en dimension neuf.

Cela a laissé la conjecture non résolue pour la dimension sept.

Lorsque Heule est arrivé à la CMU de l'Université du Texas l'année dernière, il avait déjà la réputation d'utiliser le solveur SAT pour résoudre des problèmes mathématiques ouverts de longue date.

"Je me suis dit, peut-être pouvons-nous utiliser sa technique, " se rappela Mackey. Peu de temps après, il a commencé à discuter de la façon d'utiliser le solveur SAT sur la conjecture de Keller avec Heule et Joshua Brakensiek, une double majeure en sciences mathématiques et informatique qui poursuit actuellement un doctorat. en informatique à l'Université de Stanford.

Un solveur SAT nécessite de structurer le problème à l'aide d'une formule propositionnelle - (A ou non B) et (B ou C), etc. — afin que le solveur puisse examiner toutes les variables possibles pour des combinaisons qui satisferont toutes les conditions.

"Il y a plusieurs façons de faire ces traductions, et la qualité de la traduction fait ou brise généralement votre capacité à résoudre le problème, " dit Heule.

Avec 15 ans d'expérience, Heule est habile à effectuer ces traductions. L'un de ses objectifs de recherche est de développer un raisonnement automatisé afin que cette traduction puisse se faire automatiquement, permettant à plus de personnes d'utiliser ces outils sur leurs problèmes.

Même avec une traduction de haute qualité, le nombre de combinaisons à vérifier dans la dimension sept était ahurissant – un nombre à 324 chiffres – avec une solution nulle part en vue, même avec un superordinateur. Mais Heule et les autres ont appliqué un certain nombre d'astuces pour réduire la taille du problème. Par exemple, si une configuration de données s'avérait impraticable, ils pourraient automatiquement rejeter d'autres combinaisons qui en dépendaient. Et comme la plupart des données étaient symétriques, le programme pourrait exclure les images miroir d'une configuration si elle atteignait une impasse dans un arrangement.

En utilisant ces techniques, ils ont réduit leur recherche à environ un milliard de configurations. Ils ont été rejoints dans cet effort par David Narvaez, un doctorat étudiant au Rochester Institute of Technology, qui était chercheur invité à l'automne 2019.

Une fois qu'ils ont exécuté leur code sur un cluster de 40 ordinateurs, ils ont finalement eu une réponse :la conjecture est vraie en dimension sept.

"La raison pour laquelle nous avons réussi est que John a des décennies d'expérience et de perspicacité dans ce problème et nous avons pu le transformer en une recherche générée par ordinateur, " dit Heule.

La preuve du résultat est entièrement calculée par l'ordinateur, Heule a dit, contrairement à de nombreuses publications qui combinent des parties vérifiées par ordinateur d'une épreuve avec des rédactions manuelles d'autres parties. Cela rend la compréhension difficile pour les lecteurs, il a noté. La preuve informatique de la solution Keller comprend tous les aspects de la solution, y compris une partie de rupture de symétrie apportée par Narvaez, Heule a souligné, de sorte qu'aucun aspect de la preuve n'a besoin de s'appuyer sur un effort manuel.

"Nous pouvons avoir une réelle confiance dans la justesse de ce résultat, " dit-il. Un papier décrivant la résolution de Heule, Mackey, Brakensiek et Narvaez ont remporté le prix du meilleur article lors de la conférence internationale conjointe sur le raisonnement automatisé en juin.

Résoudre la conjecture de Keller a des applications pratiques, dit Mackey. Ces cliques que les scientifiques recherchent pour réfuter la conjecture sont utiles pour générer des codes non linéaires qui peuvent accélérer la transmission des données. Le solveur SAT peut ainsi être utilisé pour trouver des codes non linéaires de dimension plus élevée qu'auparavant.

Heule a récemment proposé d'utiliser le solveur SAT pour résoudre un problème mathématique encore plus célèbre :la conjecture de Collatz. Dans ce problème, l'idée est de choisir n'importe quel nombre entier positif et de diviser par 2 s'il s'agit d'un nombre pair ou de multiplier par 3 et d'ajouter 1 s'il s'agit d'un nombre impair. Ensuite, appliquez les mêmes règles au nombre résultant et à chaque résultat successif. La conjecture est que le résultat final sera toujours 1.

Résoudre Collatz avec le solveur SAT " est un long chemin, " a reconnu Heule. Mais c'est un objectif ambitieux, il ajouta, expliquant que le solveur SAT pourrait être utilisé pour résoudre un certain nombre de problèmes mathématiques moins intimidants, même si Collatz s'avère inaccessible.