AccueilFacktualitéUne preuve assistée par ordinateur résout le problème de la "coloration de...

Une preuve assistée par ordinateur résout le problème de la « coloration de l’emballage »

Heule, cependant, a trouvé la découverte des résultats passés revigorante. Cela a démontré que d’autres chercheurs trouvaient le problème suffisamment important pour y travailler, et lui a confirmé que le seul résultat qui valait la peine d’être obtenu était de résoudre complètement le problème.

« Une fois que nous avons compris qu’il y avait eu 20 ans de travail sur le problème, cela a complètement changé la donne », a-t-il déclaré.

Éviter le vulgaire

Au fil des ans, Heule avait fait carrière en trouvant des moyens efficaces de rechercher parmi de vastes combinaisons possibles. Son approche s’appelle la résolution SAT, abréviation de « satisfiabilité ». Il s’agit de construire une longue formule, appelée formule booléenne, qui peut avoir deux résultats possibles : 0 ou 1. Si le résultat est 1, la formule est vraie et le problème est résolu.

Pour le problème de coloration de l’emballage, chaque variable de la formule peut représenter si une cellule donnée est occupée par un nombre donné. Un ordinateur cherche des moyens d’assigner des variables afin de satisfaire la formule. Si l’ordinateur peut le faire, vous savez qu’il est possible d’emballer la grille dans les conditions que vous avez définies.

Malheureusement, un encodage simple du problème de coloration de l’emballage sous forme de formule booléenne pourrait s’étendre à plusieurs millions de termes – un ordinateur, ou même une flotte d’ordinateurs, pourrait fonctionner en permanence pour tester toutes les différentes façons d’attribuer des variables en son sein.

« Essayer de faire cette force brute prendrait jusqu’à ce que l’univers se termine si vous le faisiez naïvement », a déclaré Goddard. « Vous avez donc besoin de quelques simplifications intéressantes pour le ramener à quelque chose qui est même possible. »

De plus, chaque fois que vous ajoutez un nombre au problème de coloration de l’emballage, cela devient environ 100 fois plus difficile, en raison de la multiplication des combinaisons possibles. Cela signifie que si une banque d’ordinateurs travaillant en parallèle pouvait exclure 12 en une seule journée de calcul, il lui faudrait 100 jours de temps de calcul pour exclure 13.

Heule et Subercaseaux considéraient la mise à l’échelle d’une approche informatique par force brute comme vulgaire, d’une certaine manière. « Nous avions plusieurs idées prometteuses, nous avons donc adopté l’état d’esprit suivant : » Essayons d’optimiser notre approche jusqu’à ce que nous puissions résoudre ce problème en moins de 48 heures de calcul sur le cluster «  », a déclaré Subercaseaux.

Pour ce faire, ils devaient trouver des moyens de limiter le nombre de combinaisons que le cluster informatique devait essayer.

« [They] Je veux non seulement le résoudre, mais le résoudre de manière impressionnante », a déclaré Alexander Soifer de l’Université du Colorado à Colorado Springs.

Heule et Subercaseaux ont reconnu que de nombreuses combinaisons sont essentiellement les mêmes. Si vous essayez de remplir une tuile en forme de losange avec huit nombres différents, peu importe si le premier nombre que vous placez est un en haut et un à droite du carré central, ou un en bas et un à gauche de la place centrale. Les deux emplacements sont symétriques l’un par rapport à l’autre et contraignent votre prochain mouvement exactement de la même manière, il n’y a donc aucune raison de les vérifier tous les deux.

Si chaque problème d’emballage pouvait être résolu avec un modèle d’échiquier, où une grille diagonale de 1 couvre tout l’espace (comme les espaces sombres sur un échiquier), les calculs pourraient être considérablement simplifiés. Pourtant, ce n’est pas toujours le cas, comme dans cet exemple d’une tuile finie contenant 14 nombres. Le motif de l’échiquier doit être brisé à quelques endroits vers le coin supérieur gauche.Avec l’aimable autorisation de Bernardo Subercaseaux et Marijn Heule

François Zipponi
François Zipponihttp://10-raisons.com/author/10raisons/
Je suis François Zipponi, éditorialiste pour le site 10-raisons.com. J'ai commencé ma carrière de journaliste en 2004, et j'ai travaillé pour plusieurs médias français, dont le Monde et Libération. En 2016, j'ai rejoint 10-raisons.com, un site innovant proposant des articles sous la forme « 10 raisons de... ». En tant qu'éditorialiste, je me suis engagé à fournir un contenu original et pertinent, abordant des sujets variés tels que la politique, l'économie, les sciences, l'histoire, etc. Je m'efforce de toujours traiter les sujets de façon objective et impartiale. Mes articles sont régulièrement partagés sur les réseaux sociaux et j'interviens dans des conférences et des tables rondes autour des thèmes abordés sur 10-raisons.com.

Articles récents