Trois scientifiques ont prouvé que la bicoloration des triplets de Pythagore n'était pas possible pour tous les entiers. Au-delà de la résolution d'un problème mathématique vieux de 35 ans, la méthode utilisée (solveur SAT) est très intéressante et laisse entrevoir de nombreuses possibilités dans tous les domaines scientifiques.

Les mathématiciens sont un peu joueurs et se posent parfois de drôles de questions, généralement bien difficiles à résoudre. Mais avec les ordinateurs modernes et les avancées dans le domaine de l'algorithmique, la solution est à portée pour certaines énigmes. C'est notamment le cas de... la bicoloration des triplets de Pythagore.

Deux couleurs, trois nombres et des milliards de milliards de possibilités

Le CNRS en donne la définition suivante : il s'agit de savoir s'il « est possible de colorier chaque entier positif en bleu ou en rouge de telle manière qu’aucun triplet d’entiers a, b et c qui satisfait la fameuse équation de Pythagore a²+ b²= c² soient tous de la même couleur ? Par exemple, pour le triplet 3, 4 et 5, si 3 et 5 sont coloriés en bleu, alors 4 doit être rouge ».

Si la question parait simple en apparence, on se doute qu'elle se complique de manière exponentielle lorsque le nombre de triplets à prendre en compte augmente. En 2013, les chercheurs Joshua Cooper et Chris Poirel arrivaient à trouver une solution pour « colorier » des nombres entiers jusqu'à 1 344 sans avoir de triplets qui ne comportent que des nombres de la même couleur. Pour autant, cela ne permet pas de répondre à la question pour les nombres supérieurs. Simplement peut-on affirmer que la réponse est oui jusqu'à 1 344, sans que cela ne laisse présager quoi que ce soit de plus. Frustant pour les mathématiciens, mais un défi intéressant pour d'autres.

Dans un article soumis pour publication le 3 mai, et repris récemment par le journal du CNRS, trois scientifiques (Marijn J. H. Heule, Oliver Kullmann et Victor W. Marek) sont enfin parvenus à trouver la solution ce « problème mathématique ouvert depuis 35 ans ». Et leur réponse est sans ambiguïté : non, il n'est pas possible de colorier des entiers de cette manière.

Jusqu'à 7 824 tout va bien, à 7 825 c'est impossible

 Leur étude montre tout de même qu'il est possible de colorier les entiers positifs jusqu'à 7 824 de manière à ce que tous les triplets de Pythagore aient des nombres des deux couleurs. Les scientifiques ajoutent qu'il existe même plusieurs manières d'y arriver. Les cases blanches dans la représentation ci-dessous sont sans contrainte et peuvent donc être indifféremment bleues ou rouges pour que les conditions du problème soient remplies. Néanmoins, cela devient impossible à partir de 7 825. Inutile d'aller plus loin donc.

Au-delà de cette réponse qui n'apporte rien de plus que la satisfaction de l'avoir trouvée (et qui est présenté à la conférence SAT 2016 à Bordeaux), la méthode utilisée par le trio de scientifiques est très intéressante à analyser. Laurent Simon, du Laboratoire bordelais de recherche en informatique (LaBRI), explique en effet que « pour le prouver, les chercheurs n’ont pas eu d’autres choix que d’y aller “en force” en énumérant et en vérifiant toutes les combinaisons possibles ».

Une solution qui fonctionne pour les 7 824 premiers entiers (les cases blanches sont sans contrainte de couleur)

Un supercalculateur à la rescousse

Et il y en a des combinaisons : 2^7825, soit environ 10^2355 possibilités à analyser, ou encore 1 suivi de 2 355 zéros. Afin de réduire le champ des possibilités, et donc gagner du temps de calcul (qui prendrait de toute façon trop temps), les chercheurs ont mis en œuvre différentes techniques issues de la théorie des nombres. Ils sont ainsi redescendus à 1 000 milliards (1 000 000 000 000) de combinaisons « seulement ». Sans commune mesure avec le nombre total de possibilités à analyser, mais cela reste tout de même important.

À titre de comparaison, il y a 5 x 10^20 coups possibles au jeu de dames (qui est résolu, c'est-à-dire que toutes les parties possibles et imaginables ont été calculées et enregistrées), tandis que le mathématicien Claude Shannon, estime qu'il y aurait environ 10^120 parties « intéressantes » à jouer aux échecs. Au jeu de Go, une partie comporte 1,4 x 10^768 coups possibles et les intelligences artificielles commencent seulement à prendre le dessus sur les humains, là encore sans calculer toutes les possibilités, mais en ayant recours à l'apprentissage profond et par renforcement. Nous avions détaillé tout cela au sein de cette actualité.

Daniel Le Berre, du Centre de recherche en informatique de Lens (Cril), explique que « l’astuce de l’équipe a ensuite été de découper tous ces cas possibles en un million de paquets différents pour pouvoir résoudre le problème plus facilement ». Les opérations ont ensuite été effectués sur le supercalculateur Stampede de l'université du Texas. Celui-ci comprend plus de 522 000 cœurs de traitement, peut effectuer un billiard (10^15) opérations par seconde et revendique la 116e place mondiale des supercalculateurs.

La solution « pèse » la bagatelle de 200 To

« Il aura fallu alors deux jours au supercalculateur [...] pour passer en revue toutes ces possibilités et apporter la preuve tant attendue, générant pour cela 200 téraoctets de données » indique le CNRS dans son journal. Une fois la « preuve » apportée sur un plateau d'argent par le supercalculateur, encore fallait-il la vérifier.

Le résultat est d'une « taille phénoménale, équivalente à tous les textes numérisés détenus par la bibliothèque américaine du Congrès ; c’est la plus grande preuve mathématique jamais produite » et « Il faudrait 10 milliards d’années à un être humain pour la lire »  explique le centre de la recherche scientifique. Bref, c'est là encore un ordinateur qui s'est chargé de cette besogne, mais avec un programme différent.

Les solveurs SAT au cœur de la résolution de ce problème

Le CNRS ajoute que cette petite révolution a été possible grâce aux solveurs SAT, « de nouveaux algorithmes très efficaces pour résoudre ces problèmes [...] Dans le langage informatique, SAT signifie « satisfiabilité ». Il s’agit d’un formalisme logique qui capture toute la difficulté d’un problème combinatoire pour tenter ensuite de le satisfaire ». Emmanuelle Filiot, de l'université libre de Bruxelles, expliquait en 2012, qu'un « solveur SAT est un programme qui décide automatiquement si une formule de logique propositionnelle est satisfaisable ».

Deux exemples parmi d'autres : les jeux de Sudoku (voir ici pour un exemple pratique) ou un démineur, de « très simples problèmes qui peuvent être appréhendés et résolus très facilement par ce formalisme », même si cela peut aller beaucoup plus loin. Daniel Le Berre de l'université d'Artois, explique au CNRS que s'ils étaient pendant un temps réservé à l’informatique théorique, leur utilisation explose et ils permettent désormais « de résoudre des problèmes de plus en plus difficiles ».

Traitement rapide des problèmes avec de nombreuses variables et clauses

Dans les exemples d'applications actuelles, il est question de champs assez vastes allant du diagnostic d'erreur sur les circuits électroniques à l'intelligence artificielle. En 2012, Gilles Schaeffer, directeur de recherche au CNRS, ajoutait même que « l’utilisation de solveurs SAT génériques concurrence les algorithmes ad hoc pour certains problèmes d’optimisation combinatoire ».

C'est encore trop obscur pour vous ? En 2012 toujours, le blog d'Ozwald donnait quelques exemples pratiques (même si ces informations ont quatre ans, l'idée générale reste la même) : « Là où ça devient intéressant, c'est qu'on peut faire beaucoup plus que des mini problèmes. Parmi les fichiers cnf mis à dispositions ici on en trouve un qui compte 1 040 variables et 3 668 clauses que Minisat résout (comme "UNSATISFIABLE") en... 0m0.013 s ! Dans la même catégorie on trouve un autre fichier de test contenant 1501 variables et 3575 clauses que Minisat résout (en "SATISFIABLE" avec une solution exemple) en 0m0.008 s ». Un traitement des plus rapides donc, et les choses ont encore dû s'améliorer depuis.

Vous l'aurez compris : de manière générale, les solveurs SAT permettent parfois d'obtenir de bons résultats, surtout lorsqu'il n'existe pas d'autres options que la « force brute  », ce qui est exactement le cas dans la bicoloration des triplets de Pythagore.

Pour ce dernier, c'est le programme Glucose qui a été utilisé, un solveur SAT développé par Gilles Audemard et Laurent Simon. Il a été récompensé à plusieurs reprises lors de compétitions internationales et le code source peut être téléchargé par ici. En 2014, c'est également Glucose qui avait déjà permis de construire la plus longue preuve mathématique de l'époque note le CNRS.

Microsoft et Intel utilisent déjà les solveurs SAT, d'autres applications en route

Ce dernier ajoute que, « aujourd’hui, Microsoft fait appel à ces algorithmes pour tester ses nouveaux systèmes d’exploitation. Il s’agit alors d’identifier une succession d’instructions parmi des millions susceptibles de causer un bug dans le logiciel ou au contraire de prouver qu’il n’y en aura pas. Même chose pour Intel qui vérifie grâce à ces outils le bon fonctionnement de ses microprocesseurs. Et le nombre d’applications ne cesse de croître en robotique, en bio-informatique ou encore en cryptographie ». L'intelligence artificielle et les solveurs SAT sont aussi étroitement liés, comme on peut facilement s'en douter.

Laurent Simon, coauteur du logiciel Glucose, explique que « ce dernier résultat [NDLR : la bicoloration des triplets de Pythagore] montre qu’il est possible de s’attaquer avec cette méthode à des problèmes mathématiques combinatoires extrêmement difficiles, pour lesquels aucune approche classique à la main n’est encore disponible. Il préfigure probablement la fin d’autres conjectures similaires qui résistent encore aujourd’hui aux mathématiciens ».

Il faut donc s'attendre à ce que les choses évoluent, que ce soit pour les mathématiques, l'informatique et les sciences de manière générale. Dans tous les cas, il reste une question, comme le note de manière ironique Gérad Villemin sur son blog : « Ce type de preuve établit des faits sans les expliquer. Pourquoi 7 824 ? ». On vous laisse méditer sur cette nouvelle question...