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

Avatar photo

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

Related Posts