🔢 mathematics

Queen Domination by SAT Solving

Cet article présente un cadre SAT de haute performance produisant des preuves qui résout le cas de la domination des reines pour $n=19$ , resté jusqu'alors ouvert, et corrige l'énumération pour $n=16$ en exploitant un encodage géométriquement informé, une rupture de symétrie et un pipeline de vérification unifié afin de garantir une exactitude vérifiable de manière indépendante.

Auteurs originaux : Taha Rostami, Curtis Bright

Publié 2026-07-30

📖 4 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Taha Rostami, Curtis Bright

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 un monde où les mathématiques ne se limitent pas à des chiffres sur une page, mais consistent à résoudre des énigmes si complexes que même les cerveaux humains les plus brillants en ont le vertige. C'est le domaine de la recherche combinatoire, une branche de l'informatique et des mathématiques dédiée à la recherche de la meilleure façon d'organiser les choses. Imaginez cela comme essayer de trouver le plan de table parfait pour un mariage massif où chaque invité a des règles spécifiques sur les personnes à côté desquelles il peut s'asseoir, ou déterminer le nombre absolu minimum de agents de sécurité nécessaires pour surveiller chaque recoin d'un musée sans laisser de zone d'ombre.

L'un des puzzles les plus célèbres dans ce domaine est le problème de la domination des reines. Imaginez un échiquier. Une reine est une pièce puissante qui peut attaquer tout ce qui se trouve sur sa rangée, sa colonne et ses deux diagonales. La question est simple mais délicate : quel est le plus petit nombre de reines que vous devez placer sur un plateau de $n \times n$ pour que chaque case soit attaquée ? Cela semble facile pour un petit plateau, mais à mesure que le plateau s'agrandit, le nombre de dispositions possibles explose pour atteindre des milliards, des trillions et bien plus encore. Depuis plus d'un siècle, les mathématiciens tentent de résoudre ce problème, non seulement pour trouver le nombre, mais aussi pour compter exactement de combien de façons différentes on peut disposer ces reines. Pourquoi cela importe-t-il ? Parce que la résolution de ces énigmes nous aide à comprendre comment organiser des systèmes complexes, de la planification des vols à la conception de puces informatiques. Mais il y a un piège : lorsque les ordinateurs font les mathématiques, ils peuvent commettre des erreurs, et parfois, ils passent totalement à côté de la réponse.

C'est là que Taha Rostami et Curtis Bright interviennent avec leur article, « Queen Domination by SAT Solving ». Ils se sont attaqués au problème de compter toutes les façons uniques de placer le nombre minimum de reines sur des échiquiers allant jusqu'à la taille 19. Au lieu d'écrire un programme personnalisé pour traquer les solutions comme l'ont fait les chercheurs précédents, ils ont traduit l'intégralité du puzzle de l'échiquier dans un langage qu'un solveur SAT (une machine logique super intelligente) comprend. Considérez un solveur SAT comme un détective qui vérifie si un ensemble de règles peut un jour être vrai. Si le détective dit « non », il peut le prouver avec un certificat que n'importe qui peut vérifier pour s'assurer que le détective n'a pas menti.

Les auteurs ont construit une « traduction » spéciale de l'échiquier qui mettait en évidence la géométrie du jeu, utilisant une astuce ingénieuse appelée courbe de Hilbert pour organiser les indices afin que le détective puisse trouver la réponse plus rapidement. Ils ont également utilisé une stratégie appelée Cube-and-Conquer, qui consiste à diviser un gâteau géant et impossible à manger en des milliers de petites tranches gérables que différents ordinateurs peuvent manger en même temps. Le résultat ? Ils n'ont pas seulement résolu le puzzle ; ils ont prouvé que leur solution était 100 % correcte.

Leur travail a mis au jour une erreur surprenante dans l'histoire de ce problème. Pour un plateau de 16x16, des experts précédents pensaient qu'il n'existait que 43 façons uniques de placer les reines. Rostami et Bright ont prouvé qu'il y a en réalité 371 façons — une différence massive qui suggère que l'ancien programme informatique avait un bug caché qui manquait la plupart des solutions. De plus, ils ont résolu un cas qui était ouvert depuis longtemps : le plateau de 19x19. Ils ont découvert qu'il existe exactement 11 façons uniques de dominer ce plateau avec le nombre minimum de reines. En générant des « certificats de preuve » pour chaque résultat, ils ont apporté à la communauté mathématique un niveau de confiance auparavant impossible, montiant que lorsqu'on combine un codage intelligent avec une vérification de preuve rigoureuse, on peut résoudre des problèmes que même les meilleurs logiciels spécialisés pourraient manquer.

Résumé Technique : Domination par les reines par résolution de SAT

Définition du Problème
Le problème de la domination par les reines cherche le nombre minimal de reines, noté $\gamma(Q_n)$ , nécessaires pour attaquer chaque case sur un échiquier de taille $n \times n$ . Au-delà de la détermination de cette valeur minimale, un défi important réside dans l'énumération de toutes les solutions distinctes par isomorphisme (en tenant compte des symétries du plateau telles que la rotation et la réflexion). Bien que les valeurs optimales de $\gamma(Q_n)$ aient été établies pour $n \le 25$ à l'aide d'outils de recherche spécialisés comme UNIDOM, l'énumération des solutions non isomorphes pour des plateaux plus grands reste coûteuse en calcul. Une préoccupation critique dans ce domaine est la fiabilité des résultats computationnels ; les divergences antérieures dans d'autres preuves combinatoires (par exemple, le problème de Lam) et la découverte de bogues dans des solveurs spécialisés soulignent la nécessité de certificats de correction vérifiables de manière indépendante.

Méthodologie
Les auteurs proposent un cadre de satisfaction de contraintes booléennes (SAT) produisant des preuves pour aborder le problème de la domination par les reines. Plutôt que d'implémenter un algorithme de recherche personnalisé, le problème est encodé en une formule propositionnelle sous forme de conjonction de clauses (CNF). La méthodologie repose sur plusieurs innovations techniques clés :

Encodage par Variables de Ligne : L'innovation centrale est l'introduction de variables booléennes auxiliaires représentant si des lignes géométriques spécifiques (rangées, colonnes, diagonales et anti-diagonales) contiennent au moins une reine.
- Variables de Reine ( $Q_i$ ) : Indiquent si une reine est placée sur la case $i$ .
- Variables de Ligne ( $L_\ell$ ) : Indiquent si une ligne $\ell$ est « active » (contient une reine).
- Contraintes : Les clauses garantissent que si une ligne est active, une reine existe sur celle-ci. La domination est exprimée en exigeant que pour chaque case, au moins une de ses quatre lignes intersectantes soit active. Les contraintes de cardinalité limitent le nombre total de reines ( $\sum Q_i \le \gamma$ ) et le nombre total de lignes actives ( $\sum L_\ell \le 4\gamma$ ).
Encodage de Cardinalité et Ordonnancement des Littéraux :
- Les contraintes de cardinalité sont encodées à l'aide de méthodes basées sur les totalisateurs. La contrainte de reine utilise un totalisateur standard compatible avec le cadre Cube-and-Conquer, tandis que la contrainte de ligne utilise un totalisateur modulo pour la performance.
- Ordonnancement par Courbe de Hilbert : Une stratégie novatrice d'ordonnancement des littéraux est appliquée à la contrainte de cardinalité des reines. En parcourant le plateau via une courbe de Hilbert, les cases spatialement adjacentes sont regroupées dans l'arbre de comptage. Cela préserve la localité spatiale, menant à une propagation d'unités plus forte. Les expériences ont montré que cet ordonnancement résolvait l'instance $n=14$ environ 31,5 fois plus vite que l'ordonnancement par défaut.
Bris de Symétrie : Pour éliminer l'exploration redondante de solutions symétriques, le cadre impose des contraintes d'ordre lexicographique (basées sur la méthode de Warwick Harvey) entre la configuration originale des reines et ses sept transformations géométriques non identitaires. Cela a réduit considérablement les temps de résolution lors des tests préliminaires (par exemple, une accélération de 6,64× pour $n=15$ ).
Cube-and-Conquer : Pour les instances plus grandes, l'espace de recherche est partitionné en sous-problèmes indépendants (cubes) en effectuant un branchement sur les variables auxiliaires de l'encodage du totalisateur. Cela permet une résolution parallèle et améliore la scalabilité sans dépendre des placements individuels des reines pour le partitionnement.
Génération de Preuves et Vérification : Le cadre utilise cadical-exhaust pour énumérer tous les modèles en ajoutant de manière itérative des clauses de blocage. Il génère des preuves DRAT avec des « clauses de confiance » pour certifier la complétude. Ces preuves sont vérifiées de manière indépendante via drat-trim-t, garantissant que les résultats ne dépendent pas de la logique de recherche interne du solveur, mais uniquement de l'encodage et du vérificateur de preuve.

Résultats Clés
L'étude a réussi à énumérer les solutions minimales non isomorphes de domination par les reines pour tous les $n \le 19$ . Les résultats incluent :

Correction de la Littérature : Pour $n=16$ , l'article identifie une divergence par rapport aux rapports précédents. Alors que le solveur spécialisé UNIDOM rapportait 43 solutions non isomorphes, le cadre SAT prouve qu'il y en a exactement 371. Les auteurs attribuent cela à un bug dans UNIDOM qui fait manquer des solutions valides sous certaines configurations.
Résolution d'un Cas Ouvert : Le cas précédemment ouvert de $n=19$ est résolu, établissant qu'il existe exactement 11 solutions minimales non isomorphes.
Performance : Le cadre SAT a systématiquement surpassé le solveur spécialisé UNIDOM sur les instances non triviales. Pour $n=19$ , l'approche SAT a pris environ 171 575 secondes (temps CPU) pour l'énumération, contre 714 733 secondes pour UNIDOM. L'inclusion des variables de ligne a été cruciale ; une version préliminaire sans elles a mis 22,8 fois plus de temps pour résoudre et vérifier l'instance $n=19$ .

Signification et Revendications
L'article affirme que sa contribution principale est de fournir une solution haute performance et vérifiable de manière indépendante au problème d'énumération de la domination par les reines. En passant d'un code de recherche spécialisé à un cadre SAT produisant des preuves, les auteurs réduisent la « confiance » requise dans le processus de calcul. La correction des résultats dépend désormais uniquement de l'encodage SAT et du vérificateur de preuve externe, plutôt que de la logique complexe et personnalisée d'un solveur spécialisé.

Ce travail démontre qu'une conception d'encodage minutieuse — spécifiquement l'introduction de variables auxiliaires pour exposer la structure géométrique, l'utilisation de contraintes globales et un ordonnancement de littéraux sensible à la géométrie — peut rendre la résolution de SAT produisant des preuves compétitive avec, voire supérieure, à celle de solveurs spécialisés hautement optimisés. Les auteurs rendent leur code source et leurs données de solution publics afin de faciliter toute vérification et recherche ultérieures.

Articles similaires