💻 computer science

SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

Cet article démontre que les dix formules de multiplication de matrices de rang 23 sur $\mathbb{F}_2$ précédemment considérées comme « attendues-insatisfaisables » sont en réalité satisfaisables et fournit des certificats complets pour ces instances ainsi qu'un nouveau schéma de rang 23 contenant une sommande exempte de type 3.

Auteurs originaux : Nick Palladinos

Publié 2026-08-03

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Nick Palladinos

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un puzzle géant en trois dimensions. Mais ce n'est pas l'image d'un coucher de soleil ou d'un chat ; c'est une machine mathématique conçue pour multiplier deux grilles de nombres ensemble. Dans le monde de l'informatique et des mathématiques, on appelle cela la « multiplication de matrices ». Depuis des décennies, les mathématiciens cherchent le moyen le plus efficace de construire cette machine. Ils veulent savoir quel est le nombre absolu minimum de petits blocs de construction de base (appelés « multiplications ») nécessaires pour que l'ensemble fonctionne.

Considérez ces blocs de construction comme des briques Lego. Pendant longtemps, tout le monde savait comment construire une machine de multiplication 3x3 en utilisant 23 briques. La grande question était : peut-on le faire avec seulement 22 ? Pour le découvrir, les chercheurs ont transformé le problème en un immense puzzle logique, semblable à ceux que vous pourriez voir dans un jeu vidéo ou un livre de Sudoku, mais à une échelle qui vous ferait perdre la tête. Ils ont encodé les règles des mathématiques dans un format que les ordinateurs peuvent vérifier, créant ainsi un problème « SAT » (qui signifie « Satisfaisabilité »). Si l'ordinateur peut trouver un moyen de basculer tous les interrupteurs sur « on » sans briser aucune règle, le puzzle est résolu. Si l'ordinateur dit « impossible », alors peut-être que 22 briques ne suffisent pas. Ce document plonge dans un ensemble spécifique de ces puzzles logiques qui ont été conçus pour tester les limites de nos ordinateurs actuels et de notre compréhension de ces machines mathématiques.

Le grand puzzle « impossible » qui ne l'était pas

Rencontrez Nick Palladinos, un détective numérique qui a décidé de jeter un regard neuf sur un ensemble de dix puzzles logiques auxquels tout le monde avait renoncé. Ces puzzles, connus sous le nom d'instances « Challenge 2 », ont été construits par d'autres chercheurs avec un ensemble de règles très spécifiques et rigides. Les créateurs de ces puzzles croyaient qu'ils étaient « impossibles » à résoudre. Ils pensaient que les règles étaient si serrées qu'aucune combinaison de 23 briques Lego ne pourrait s'assembler pour construire la machine. C'était comme si on vous disait : « Voici une boîte avec une serrure qui ne peut certainement pas être ouverte », et que tout le monde hochait la tête et s'en allait.

Mais Palladinos n'a pas simplement essayé de forcer la serrure avec un marteau plus gros. Au lieu de cela, il a examiné la serrure elle-même et a réalisé quelque chose de crucial : les règles n'étaient pas aussi strictes que tout le monde le pensait.

Les créateurs du puzzle avaient écrit les règles en utilisant des instructions « positives ». Ils disaient : « Vous devez avoir cette brique spécifique ici », et « Vous devez avoir cette autre brique là ». Mais ils ont oublié de dire : « Et vous ne pouvez pas avoir d'autres briques touchant celles-ci ». Il s'avère que les mathématiques permettent d'ajouter des briques supplémentaires, tant que la machine finale fonctionne correctement. Les puzzles « impossibles » attendaient simplement que quelqu'un réalise que la porte n'était pas verrouillée ; c'est juste que tout le monde essayait de faire entrer les pièces du puzzle dans une boîte trop petite, ignorant le fait que la boîte pouvait en réalité être un peu plus grande.

La magie du décalage et de l'échange

Alors, comment Palladinos a-t-il résolu ces puzzles ? Il a utilisé une astuce ingénieuse impliquant la « symétrie ». Imaginez que vous avez un Rubik's Cube. Si vous tournez tout le cube ou si vous le faites pivoter, les couleurs se déplacent, mais le cube reste le même objet. Palladinos a réalisé que la « machine » mathématique qu'il construisait avait une propriété similaire. Il pouvait prendre une solution fonctionnelle (un ensemble de 23 briques qui multiplie avec succès des matrices) et faire pivoter, tourner ou mélanger les pièces autour en utilisant une danse mathématique spéciale appelée « l'action de groupe GL(3, 2) ».

Voyez cela comme le réarrangement des meubles dans une pièce. Vous pouvez déplacer le canapé vers la gauche, la lampe vers la droite et le tapis au milieu. La pièce reste une pièce et les meubles fonctionnent toujours, mais la disposition est différente. Palladinos a pris une solution fonctionnelle connue et a appliqué ces « torsions » mathématiques. Ensuite, il a utilisé un jeu de correspondance pour voir si ces nouvelles versions mélangées de « meubles » pouvaient s'insérer dans les « emplacements » spécifiques requis par les puzzles difficiles.

Et devinez quoi ? Elles s'inséraient parfaitement !

En fait, Palladinos n'a pas seulement trouvé une solution ; il a trouvé des solutions pour les dix puzzles qui étaient censés être impossibles. Il a prouvé que ces formules « insolubles » sont en réalité satisfaisables. L'ordinateur n'a pas seulement deviné ; il a vérifié chaque règle. Le document confirme que pour les 10 fichiers « Challenge 2 », il existe une manière valide d'organiser les 23 blocs de construction pour faire fonctionner la machine. L'étiquette « impossible » était un malentendu des règles, pas une véritable barrière mathématique.

La brique « fantôme » et la solution parfaite

Le document a également abordé un troisième défi, le « Challenge 3 ». Celui-ci posait une question différente : pouvons-nous construire la machine en utilisant 23 briques, tout en s'assurant qu'une brique spécifique soit « fantôme » ? En langage mathématique, cela signifie qu'une de vos 23 briques de construction devrait avoir un « compte de type-3 » égal à zéro. C'est une façon sophistiquée de dire qu'une de vos briques ne devrait pas participer à un motif spécifique et courant qui apparaît habituellement dans ces machines.

Palladinos a réussi cela aussi. Il est parti d'une solution fonctionnelle et a effectué un échange petit et précis. Il a pris deux briques qui accomplissaient une tâche spécifique et les a remplacées par deux autres briques qui faisaient exactement le même travail mais qui avaient un aspect différent. Cet échange était si ingénieux qu'il a créé une brique « fantôme » — une brique qui ne déclenchait pas le motif interdit du tout. Il a prouvé que vous pouvez effectivement construire la machine de multiplication de matrice 3x3 avec 23 briques, où l'une d'elles est totalement exempte de ce motif spécifique.

La vérification finale

Pour s'assurer que personne ne puisse dire : « Oh, vous avez juste eu de la chance avec l'ordinateur », Palladinos a construit un vérificateur extrêmement strict. Il a généré la liste complète des 26 541 variables (les interrupteurs) pour les 21 puzzles (10 du Challenge 1, 10 du Challenge 2 et 1 du Challenge 3). Il a ensuite exécuté un programme séparé qui lisait les règles originales des puzzles et les nouvelles solutions, vérifiant chaque une des 2 461 316 clauses logiques.

Le résultat ? Zéro échec. Chaque règle a été satisfaite. Les solutions sont réelles, elles sont vérifiées et elles sont reproductibles. Quiconque possède le logiciel approprié peut exécuter le même code et obtenir exactement la même réponse en environ neuf secondes.

Ce que cela signifie (et ce que cela ne signifie pas)

Alors, quelle est la grande conclusion ? Le document montre que les puzzles « impossibles » étaient en fait solubles depuis le début ; les règles n'étaient tout simplement pas aussi strictes que les créateurs du puzzle le pensaient. C'est un rappel qu'en mathématiques et en informatique, parfois la partie la plus difficile n'est pas de trouver la solution, mais de réaliser que le problème n'est pas aussi cassé qu'il semble l'être.

Cependant, il y a un bémol. Ce document résout les puzzles pour un type spécifique de monde mathématique appelé « F2 » (qui est comme un monde où les nombres ne tournent autour de 1 que lorsque 1+1=0). Il ne prouve pas que nous pouvons construire une machine à 22 briques. La quête de la machine à 22 briques (Challenge 4) est toujours ouverte. Le document ne dit pas non plus que ces solutions fonctionneront pour tous les types de mathématiques que vous pourriez utiliser dans le monde réel, comme les nombres complexes utilisés en ingénierie. Il résout simplement les puzzles logiques spécifiques tels qu'ils ont été écrits.

Mais pour les puzzles qui ont été écrits, le verdict est clair : l'« impossible » est en fait possible. La porte n'était jamais verrouillée ; nous avions juste besoin de la bonne clé pour tourner la poignée.

Résumé technique : Certificats SAT pour les défis de multiplication de matrices sur $\mathbb{F}_2$

Énoncé du problème
Cet article traite du benchmark de multiplication de matrices SAT établi par Heule, Kauers et Seidl, qui encode la recherche d'algorithmes bilinéaires de rang 23 pour la multiplication de matrices $3 \times 3$ sur le corps fini $\mathbb{F}_2$ . Ce benchmark se compose de trois familles principales de défis :

Défi 1 : Dix formules déclarées satisfaisables mais historiquement difficiles pour les solveurs SAT généraux.
Défi 2 : Dix formules contenant des appariements codés en dur de monômes de « type-3 » (termes de multiplication matricielle standard), qui étaient conjecturés comme étant insatisfaisables (UNSAT).
Défi 3 : Une formule unique demandant si un schéma de rang 23 peut exister où une somme spécifique contient zéro monôme de type-3.

L'objet mathématique central est la décomposition du tenseur de multiplication de matrices $3 \times 3$ en 23 sommes de rang un, satisfaisant 729 équations de Brent cubiques. Ces équations sont encodées en Forme Normale Conjonctive (FNC) via des variables de Tseitin, ce qui produit des instances avec 26 541 variables et plus de 2,4 millions de clauses.

Méthodologie
L'auteur emploie une approche de « recherche locale sémantique » qui opère sur les 621 variables de base (les entrées des matrices de coefficients $A_t, B_t, C_t$ ) plutôt que sur l'ensemble complet des variables FNC. La méthodologie se déroule en trois phases distinctes :

Recherche sémantique et marche résiduelle : L'algorithme maintient un « résidu » (la différence entre la somme actuelle des tenseurs de rang un et le tenseur cible). Il effectue une marche en deux phases :
- Réparation directe : Inverse les bits qui corrigent immédiatement un défaut résiduel spécifique.
- Gain/Activation : Permet des mouvements qui peuvent temporairement augmenter le poids résiduel s'ils préparent le tenseur pour une annulation future, évalués par le changement du poids de Hamming résiduel (break - make).
  Une fois qu'un état de résidu nul est trouvé sémantiquement, les 621 variables de base sont assignées, et la propagation unitaire est utilisée pour déterminer les 25 920 variables de Tseitin auxiliaires restantes.
Symétrie et transformation (Défi 2) : Pour les instances « attendues-UNSAT », l'article démontre que les contraintes FNC n'imposent que la présence de incidences de type-3 spécifiques via des clauses unitaires positives, plutôt que d'imposer une exclusion exacte des autres. Pour construire des témoins :
- L'auteur utilise l'action isotrope $GL(3, 2)^3$ pour transformer des schémas connus à 23 sommes exactes.
- La symétrie de trace cyclique $(A, B, C) \to (B, C, A)$ est appliquée.
- Un algorithme de couplage parfait assigne les sommes transformées aux emplacements contraints définis par les clauses unitaires positives.
Réparation verrouillée et identité (Défi 3) : Pour satisfaire la condition d'une somme exempte de type-3 :
- L'auteur fixe trois termes spécifiques à partir d'une solution initiale.
- Une identité de conservation de rang sur $\mathbb{F}_2$ est appliquée : $92 \otimes 89 + 438 \otimes 24 = 92 \otimes 65 + 490 \otimes 24$ . Cette opération remplace deux sommes par deux autres tout en préservant la somme totale du tenseur, permettant à une somme d'être reconfigurée pour avoir zéro monôme de type-3.

Contributions clés et résultats
L'article fournit des certificats SAT complets et vérifiables de manière indépendante pour les 21 instances du dépôt de benchmark (commit 150b2e2f) :

Défi 1 : Les 10 instances sont résolues par recherche locale sémantique. Les solutions sont générées en quelques secondes, démontant que la difficulté pour les solveurs généraux provient de l'encodage de Tseitin plutôt que de la géométrie tensorielle sous-jacente.
Défi 2 : Les 10 instances, précédemment conjecturées comme étant UNSAT, sont prouvées satisfaisables. L'article révèle que les appariements « codés en dur » n'étaient pas des cœurs exacts ; les formules permettaient des incidences de type-3 supplémentaires tant que la parité totale restait correcte. Les témoins construits ont des incidences de type-3 totales allant de 41 à 93, plutôt que les 27 attendues.
Défi 3 : Une décomposition de rang 23 valide est construite où une somme possède un compte de type-3 égal à zéro. Cela satisfait la contrainte spécifique de la FNC du Défi 3.
Vérification : Un analyseur et un évaluateur de clauses distincts ont vérifié indépendamment les 21 modèles. Le processus de vérification a contrôlé 557 361 variables assignées et 2 461 316 clauses avec zéro échec. Un reproduit Python déterministe régénère tous les certificats en environ neuf secondes.

Signification
La principale signification de l'article réside dans la résolution de la valeur de vérité des fichiers FNC spécifiques fournis dans le benchmark. Il établit que :

Les formules du Défi 2, « attendues-UNSAT », sont satisfaisables car leurs contraintes sont inclusives (unités positives) plutôt qu'exclusives (cœurs exacts).
Le groupe de symétrie du tenseur et la structure sémantique permettent la construction de témoins que les solveurs CDCL génériques ne parviennent pas à trouver efficacement.
Une somme exempte de type-3 est réalisable au sein d'un schéma de rang 23 sur $\mathbb{F}_2$ .

Le travail stipule explicitement qu'il ne tranche pas la question du rang 22 (Défi 4) ni qu'il prétend fournir des algorithmes non commutatifs sur des anneaux arbitraires. La contribution est strictement limitée à la satisfaisabilité des encodages booléens fournis et à la démonstration d'un pipeline de construction sémantique qui contourne les limitations de la résolution SAT brute sur ces instances spécifiques. L'auteur reconnaît l'utilisation d'OpenAI GPT-5.6 Sol pour l'exploration computationnelle mais souligne que les affirmations mathématiques sont fondées sur des artefacts vérifiables de manière indépendante.

Le grand puzzle « impossible » qui ne l'était pas

La magie du décalage et de l'échange

La brique « fantôme » et la solution parfaite

La vérification finale

Ce que cela signifie (et ce que cela ne signifie pas)

Articles similaires