Constructing strong starters of orders $3p$: triplication with SAT solver

Cet article présente une méthode de « triplication » utilisant un solveur SAT pour construire des démarreurs forts d'ordre $3p$à partir de démarreurs d'ordre$p$, contribuant ainsi à la résolution de la conjecture de Horton.

L'essentiel

🧩 Le Grand Puzzle des Nombres : Comment multiplier la magie des "Starters"

Imaginez que vous êtes un architecte de l'infini, mais que vous ne travaillez qu'avec des nombres. Votre mission ? Construire des structures mathématiques parfaites appelées "Starters forts" (Strong Starters).

Ces structures sont comme des puzzles magiques. Vous prenez un ensemble de nombres (par exemple de 1 à 20) et vous devez les regrouper par paires. La règle est stricte :

1. La somme de chaque paire doit être unique.
2. La différence entre les deux nombres de chaque paire doit aussi être unique.
3. Aucune somme ou différence ne doit être nulle.

C'est facile à faire pour certains nombres, mais dès qu'on arrive à des nombres divisibles par 3 (comme 21, 33, 39...), c'est un cauchemar. Personne ne sait vraiment comment construire ces puzzles pour ces nombres-là, sauf peut-être pour quelques cas très petits. C'est là que cette étude intervient.

🚀 L'Idée Géniale : La "Triplication"

Les auteurs (Oleg, Sergey et Margo) ont découvert une astuce incroyable qu'ils appellent la "Triplication".

Imaginez que vous avez un petit puzzle parfait de taille 7. Vous voulez en créer un nouveau, trois fois plus grand, de taille 21. Au lieu de chercher une solution à partir de zéro (ce qui est comme essayer de construire un gratte-ciel sans plan), ils disent : "Prenez votre petit puzzle de 7, et appliquons une formule magique pour en faire un de 21."

Mais cette formule magique a un petit problème : elle nécessite de résoudre un Sudoku spécial (un Sudoku modulaire).

🧠 Le Sudoku Modulaire : Le Verrou de Sécurité

Voici comment fonctionne la magie, étape par étape :

1. La Base : Vous prenez votre petit puzzle de départ (le "starter" de taille 7).
2. La Clé : Vous choisissez un nombre secret, une "clé" (comme un mot de passe).
3. Le Tableau : Vous créez un tableau géant avec 3 colonnes. La première colonne est votre puzzle original. Les deux autres colonnes sont des versions déformées de ce puzzle, calculées avec votre clé.
4. Le Problème : Ce tableau est presque complet, mais il manque des pièces. Il faut remplir ces cases avec des chiffres 0, 1 ou 2 (comme un mini-Sudoku).
   • Il y a des règles strictes : dans chaque ligne, les différences doivent être différentes. Les sommes doivent respecter certaines lois.
   • C'est ici que les mathématiques deviennent un casse-tête logique.

🤖 Le Super-Héros Informatique : Le Solveur SAT

Résoudre ce Sudoku à la main est possible pour les petits nombres, mais pour les grands, c'est impossible pour un humain. C'est là qu'intervient le Solveur SAT (comme le logiciel z3 utilisé par les auteurs).

Imaginez le Solveur SAT comme un détective ultra-rapide ou un robot qui ne dort jamais.

• Vous lui donnez les règles du Sudoku (les contraintes).
• Il teste des milliards de combinaisons par seconde.
• Il vous dit : "Aha ! J'ai trouvé la combinaison de 0, 1 et 2 qui respecte toutes les règles !"

Une fois qu'il a trouvé cette solution, les auteurs utilisent une vieille technique mathématique (le Théorème des Restes Chinois) pour fusionner le petit puzzle original et la solution du Sudoku. Résultat : Ils obtiennent instantanément un nouveau puzzle parfait de taille 21 (ou 33, 39, etc.).

📊 Ce qu'ils ont découvert (Les Résultats)

Les auteurs ont testé cette méthode sur un ordinateur puissant :

• Cela fonctionne ! Pour beaucoup de nombres divisibles par 3, ils ont réussi à créer ces puzzles parfaits là où personne ne savait le faire avant.
• La vitesse : C'est très rapide pour les petits nombres (quelques secondes), mais cela devient plus lent pour les très grands nombres (plusieurs minutes ou heures).
• La surprise : Parfois, même avec les bonnes règles, le Sudoku n'a pas de solution. Cela signifie que pour certains nombres, la "triplication" ne fonctionne pas, et il faut chercher une autre méthode.

🎭 L'Analogie Finale : Le Traducteur Secret

Pour résumer simplement :
Imaginez que vous voulez envoyer un message secret à un ami dans un pays lointain (le grand nombre 3p).

1. Vous écrivez le message dans votre langue maternelle (le petit nombre p).
2. Vous utilisez un code secret (la clé) pour le transformer en un code intermédiaire (le Sudoku).
3. Un traducteur automatique (le Solveur SAT) trouve la bonne traduction dans la langue du pays lointain.
4. En combinant le message original et la traduction, vous obtenez un message complet et parfait que personne n'aurait pu écrire seul.

💡 Pourquoi c'est important ?

Ce papier ne résout pas seulement un casse-tête mathématique abstrait. Il prouve qu'on peut construire des structures complexes à partir de structures simples. C'est une nouvelle façon de voir les mathématiques : au lieu de chercher l'aiguille dans la botte de foin, on apprend à fabriquer l'aiguille à partir d'un morceau de métal plus petit.

Les auteurs espèrent que dans le futur, ils pourront créer un algorithme encore plus rapide que le robot actuel pour résoudre ces Sudoku, rendant la construction de ces puzzles encore plus simple et accessible.

Résumé technique

1. Problématique et Contexte

L'article aborde la construction de démarrages forts (strong starters) dans les groupes cycliques d'ordre $n$, où $n$ est un multiple de 3.

• Définition : Un démarrage fort dans un groupe abélien additif d'ordre impair $n$ est une partition de l'ensemble $G \setminus \{0\}$ en $k = (n-1)/2$ paires $\{a_i, b_i\}$ telle que :
  1. Toutes les sommes $a_i + b_i$ sont distinctes et non nulles modulo $n$.
  2. Toutes les différences $\pm(a_i - b_i)$ sont distinctes et non nulles modulo $n$.
• Le défi théorique : L'existence de démarrages forts est bien établie pour les ordres $n$ non divisibles par 3. Cependant, pour les ordres $n$ divisibles par 3 (sauf $n=3$ et $n=9$), l'existence reste une conjecture de Horton (1989) non prouvée. Les résultats théoriques existants ne garantissent l'existence que pour certaines plages d'ordres (par exemple $n < 1000$ ou sous certaines conditions de facteur premier).
• Objectif : Proposer une méthode constructive pour générer des démarrages forts d'ordre $3p$(où$p$est premier à 3) à partir d'un démarrage fort d'ordre$p$, comblant ainsi un vide théorique et pratique.

2. Méthodologie : La Triplication et le Sudoku Modulaire

Les auteurs proposent une méthode novatrice appelée « triplication ». Cette approche transforme le problème de construction d'un démarrage d'ordre $3p$ en un problème de satisfaction de contraintes (CSP) modulo 3.

A. Le Principe de Triplication

La méthode prend en entrée :

1. Un démarrage fort $T$ d'ordre $p$ (coprime à 3).
2. Une « clé » $t \in \{0, \dots, p-1\}$.

Elle construit une table de triplication $\Sigma_p$ de taille $3q+1$(où$q=(p-1)/2$) contenant des paires modulo$p$. Cette table est composée de trois colonnes :

• La première colonne est le démarrage de base $T$.
• Les deux autres colonnes sont des dérivées de $T$ utilisant la clé $t$ (translations et réflexions modulaires).
• Une paire « sommet » $(t, t)$ est ajoutée.

B. Le Problème de Sudoku Modulaire

L'étape cruciale consiste à trouver une table de valeurs $\Sigma_3$ (modulo 3) qui, combinée à $\Sigma_p$ via le Théorème Chinois des Restes (CRT), forme un démarrage fort d'ordre $3p$.
Les variables de $\Sigma_3$ (notées $U_i, V_i$) doivent satisfaire trois types de contraintes strictes :

1. Contraintes de ligne : Les différences $U_i - V_i$ dans chaque ligne régulière doivent être distinctes modulo 3 (couvrant $\{0, 1, 2\}$).
2. Contraintes d'ensembles faibles (Weak Sets) : Pour les paires dans $\Sigma_p$ ayant la même somme modulo $p$, leurs sommes correspondantes modulo 3 doivent être distinctes (et non nulles si la somme modulo $p$ est nulle).
3. Contraintes de couleurs (Monochrome Sets) : Les positions des mêmes valeurs numériques dans $\Sigma_p$ doivent contenir des valeurs distinctes modulo 3.

Ce système de contraintes est formulé comme un problème de type « Sudoku modulaire ».

C. Résolution par Solveur SAT

Pour résoudre ce problème de satisfaction de contraintes, les auteurs utilisent le solveur généraliste z3 (bibliothèque Microsoft). L'implémentation en Python encode les contraintes décrites ci-dessus et recherche une affectation valide des variables modulo 3.

3. Contributions Clés

1. Algorithme de Triplication : Introduction d'une méthode systématique pour étendre un démarrage d'ordre $p$ vers un ordre $3p$, réduisant un problème combinatoire complexe à un problème de satisfaction de contraintes modulo 3.
2. Théorèmes de Validité :
   • Théorème 1 : Prouve que toute solution valide du problème de Sudoku modulaire génère effectivement un démarrage fort d'ordre $3p$.
   • Théorème 2 : Établit une condition nécessaire pour la solvabilité : la clé $t$ ne doit ni être nulle, ni appartenir à l'ensemble des sommes des paires du démarrage de base $T$ ($t \notin \hat{T} \cup \{0\}$).
   • Théorème 3 : Démontre une symétrie involutive des solutions (permutation des valeurs 1 et 2 modulo 3).
3. Algorithme de Reconnaissance Inverse : Proposition d'un test algorithmique pour déterminer si un démarrage fort d'ordre $3p$donné peut être issu d'une triplication (en vérifiant la structure des lignes modulo$p$).
4. Preuve de Concept par SAT : Démonstration pratique que les solveurs SAT modernes peuvent résoudre efficacement ces problèmes de Sudoku modulaire, même pour des ordres relativement grands.

4. Résultats Expérimentaux

Les auteurs ont implémenté la méthode en Python avec z3 et effectué des tests sur plusieurs séries de données :

• Performance :
  • Pour des ordres de base $p < 100$, le temps de résolution est très faible (de 0,06 s pour $p=7$ à ~90 s pour $p=97$).
  • Pour des ordres plus grands ($100 < p < 500$), le temps de calcul augmente de manière non monotone mais reste gérable (quelques milliers de secondes pour$p \approx 500$).
  • Une corrélation heuristique avec la formule $\tau \approx m^2 \ln m$ est observée pour les petits ordres, bien que des sauts importants apparaissent pour les grands ordres, suggérant une complexité plus élevée ou des cas difficiles spécifiques.
• Comparaison :
  • La méthode de triplication est nettement plus rapide que l'utilisation directe d'un solveur SAT pour trouver un démarrage fort d'ordre $3p$(ex: 200s pour$n=39$ en direct vs <1s via triplication).
  • Cependant, elle est plus lente que les algorithmes de « hill-climbing » (montée de colline) de Dinitz et Stinson pour la génération pure, mais offre une approche constructive déterministe basée sur une base existante.
• Fréquence des solutions :
  • La condition nécessaire du Théorème 2 semble aussi être une condition suffisante dans les cas testés (Conjecture).
  • L'analyse de démarrages « aléatoires » d'ordre 21, 33 et 39 montre que très peu d'entre eux (environ 1,8% pour $n=21$, 0% pour $n=39$) peuvent être obtenus par triplication, indiquant que cette méthode ne couvre qu'une sous-classe spécifique des démarrages forts.

5. Signification et Perspectives

• Avancée Théorique : Cette méthode fournit un cadre constructif pour la conjecture de Horton, prouvant l'existence de démarrages forts pour une large classe d'ordres $3p$ (à condition que le problème de Sudoku modulaire ait une solution).
• Efficacité Pratique : L'utilisation de solveurs SAT pour des problèmes de combinatoire modulaire s'avère très efficace, offrant une alternative viable aux méthodes heuristiques purement aléatoires.
• Limites et Futur :
  • La méthode ne génère pas tous les démarrages forts possibles (seulement ceux issus d'une triplication).
  • Les auteurs prévoient de développer un algorithme spécialisé pour résoudre le problème de Sudoku modulaire, qui devrait surpasser les solveurs SAT génériques en performance.
  • L'étude de la structure des ensembles faibles et de leur corrélation avec le temps de résolution ouvre de nouvelles pistes de recherche.

En résumé, cet article présente une contribution majeure à la théorie des designs combinatoires en reliant la construction de démarrages forts à la résolution de problèmes de contraintes modulaires, validée par des expériences computationnelles robustes.