Vers l’EXPTIME-difficulté de Raumschach : une construction de gadget vérifiée
Une réduction candidate depuis Generalized Geography, avec une correction de gadgets vérifiée mécaniquement — soumise pour évaluation par les pairs
1. Introduction
Le résultat classique de Fraenkel et Lichtenstein (1981) montre que décider du vainqueur d’une position d’échecs généralisés n×n requiert un temps exponentiel en n pour tout algorithme fixé, via une réduction depuis un jeu de formule alternée PSPACE-difficile joué sur un graphe planaire. Un obstacle technique persistant dans cette construction, et dans les travaux ultérieurs qui l’étendent, est que le graphe de flux de contrôle de la réduction n’est généralement pas planaire, forçant un gadget explicite de « croisement de fils » pour router un signal logique par-dessus un autre sur un plateau bidimensionnel.
Raumschach, la variante d’échecs tridimensionnelle 5×5×5 conçue par Ferdinand Maack (1907), supprime cet obstacle pour une raison structurelle : un plateau avec une véritable troisième dimension spatiale admet deux couloirs qui ne partagent pas un plan, de sorte que le croisement n’est pas un cas particulier nécessitant son propre gadget — ce sont simplement deux chemins disjoints. Cet article développe cette observation en une réduction candidate et rapporte, intégralement, à la fois l’état actuel de la réduction et une erreur trouvée et corrigée au cours de sa vérification.
Ces travaux suivent un arc de développement consigné en interne dans les Notes techniques de l’IRF 1 à 15 (les Notes 1 à 14 conservées comme archive institutionnelle, non publiées séparément) et l’article consolidé Raumschach et complexité computationnelle, que cet article remplace spécifiquement en ce qui concerne la construction condition de victoire/porte AND (Section 6 de cet article), conformément à l’erratum de la Note technique 15, qui est publiée. Les lecteurs souhaitant l’analyse de l’espace d’états et de la taille de l’arbre de jeu, qui n’est affectée par rien dans cet article, devraient consulter directement cet article.
Ce que cet article est, et n’est pas. Ceci est un rapport technique décrivant une esquisse de réduction, un ensemble de gadgets, et un programme de vérification informatique de ces gadgets sur des instances finies — y compris un exemple non trivial entièrement traité avec six variables booléennes, un jeu alterné réel, et un échec et mat confirmé. Ce n’est pas une preuve mathématique générale et achevée que la réduction est correcte pour une taille de formule arbitraire, et nous ne revendiquons pas ici l’EXPTIME-difficulté comme un théorème établi. Nous décrivons exactement où se situe actuellement l’écart entre « vérifié sur les instances que nous avons contrôlées » et « prouvé pour toutes les instances », à la Section 8.
2. Préliminaires
2.1 Raumschach
Raumschach se joue sur un plateau 5×5×5, coordonnées (L, f, r) ∈ {1,…,5}3 dans la notation standard (niveau, colonne, rangée). Les pièces incluent la Tour, le Fou, la Dame, le Roi, et le Pion habituels, plus la Licorne, qui se déplace le long de rayons purement triagonaux — les trois coordonnées changeant de ±1 à chaque pas. Pour la réduction, nous opérons sur un plateau agrandi n×n×n, n polynomial en la taille de la formule, suivant la pratique standard dans ce domaine de travaux consistant à utiliser un plateau surdimensionné pour intégrer une réduction, puis à argumenter que la construction respecte tout ensemble de pièces et règles de déplacement que définit le jeu de base.
2.2 Le problème source
Nous réduisons à partir d’un jeu de formule à deux joueurs, à coups alternés, dans le style des formulations Generalized Geography / jeu-QBF utilisées dans les constructions de type Fraenkel–Lichtenstein : une formule booléenne φ(x1,…,xn) dans une base fixe (ici, AND et OR suffisent, par la loi de De Morgan et la disponibilité d’un véritable NOT via l’attribution du joueur — voir Section 7), accompagnée d’une partition des variables entre deux joueurs, Joueur A et Joueur B, et d’un ordre fixe dans lequel elles sont fixées. Le Joueur A gagne si l’attribution résultante satisfait φ ; le Joueur B gagne sinon. Décider quel joueur possède une stratégie gagnante pour de tels jeux est PSPACE-complet en général, et la littérature sur la réduction aux échecs compose en outre cela avec des considérations de taille de plateau pour obtenir l’EXPTIME-difficulté du problème de décision sur des plateaux de taille appropriée. Nous ne re-dérivons pas ici cette ossature générale de théorie de la complexité ; nous la prenons comme cible et nous concentrons sur la réduction au niveau du plateau.
2.3 Ce qu’une réduction correcte doit accomplir
Une réduction de ce jeu vers la détermination du vainqueur d’une position de Raumschach doit exhiber, pour chaque formule φ et chaque partition/ordre de variables, une position de Raumschach telle que : (a) la position peut être construite en temps polynomial en |φ| ; (b) les coups des deux joueurs dans la partie d’échecs résultante correspondent exactement à leurs choix d’attribution de variable, dans le même ordre ; et (c) les Blancs (sans perte de généralité, le joueur représentant A) ont un gain forcé dans la partie d’échecs si et seulement si A possède une stratégie gagnante dans le jeu de formule. Chaque gadget de la Section 4 existe pour faire tenir une partie de cette correspondance ; la Section 5 énonce, gadget par gadget, de quelle partie il est responsable.
3. Vue d’ensemble de la réduction
Le plateau est divisé en régions disjointes : une région par variable de formule (un couloir se terminant en un point de branchement binaire, selon la Section 4.1), une région par connecteur logique dans l’arbre syntaxique de la formule (une instance de porte OR ou AND, Sections 4.3–4.4), un remplissage de fusible de synchronisation des tempos partout où deux couloirs de longueur naturelle différente alimentent le même point dans l’ordre d’alternance (Section 4.5), et un unique gadget de condition de victoire (Section 4.6) dont la propre légalité est câblée — non composée par case partagée, voir Section 5.4 — à la valeur de vérité finale de la formule. La sécurité du roi est établie une fois pour toutes, indépendamment de la formule (Section 4.6.1), en utilisant six des sept directions de case de fuite tridimensionnelles du Roi scellées par du matériel bloquant ordinaire, la septième étant laissée ouverte spécifiquement pour être fermée par le propre mécanisme d’échec par découverte du gadget de condition de victoire.
4. Gadgets
4.1 Couloir de variable
Chaque variable xi contrôlée par un joueur donné est représentée par un Pion confiné à une seule colonne, avançant d’une case par coup (les Pions de Raumschach, comme leur homologue bidimensionnel, se déplacent d’exactement une case vers l’avant par coup sans prise), avec l’ascension (le second type de coup à un seul pas du Pion, changeant le niveau d’une unité) bloquée par une Tour immobile à chaque case le long du couloir sauf la dernière. À la dernière case, l’avancée frontale et l’ascension sont toutes deux laissées ouvertes : l’ascension représente xi = Vrai (le Pion quitte entièrement le niveau du couloir), l’avancée frontale continuée représente xi = Faux. Ceci est un véritable branchement binaire à choix unique, résolu par un coup réel contre le véritable générateur de coups légaux, non une valeur supposée à l’avance.
4.2 Passage de niveau
Là où un chemin de signal dans l’arbre syntaxique de la formule devrait, sur un plateau bidimensionnel, croiser un autre chemin de ce type, la troisième dimension de Raumschach est utilisée directement : le chemin croisant est acheminé à travers un niveau adjacent, avec une ascension de Pion changeant de niveau (ou un pas de Fou/Licorne, selon le type de pièce du couloir) servant de « passage ». Aucun gadget de croisement dédié du type que requiert la construction planaire de Fraenkel–Lichtenstein n’est nécessaire ; deux couloirs sur des niveaux différents ne s’intersectent tout simplement pas.
4.3 Porte OR
Un unique jeton Tour reçoit exactement deux directions de tour actives, chacune murée indépendamment par un jeton de négation : présent (bloquant) si l’entrée correspondante est Faux, absent si Vrai. Les quatre autres directions sont murées en permanence. Le jeton dispose d’un coup légal si et seulement si au moins l’une de ses deux directions filtrées est ouverte, c.-à-d. si et seulement si au moins une entrée est Vraie — réalisant OR. Ce gadget est inchangé par rapport à la Section 7 de l’article consolidé et n’est pas affecté par l’erreur décrite à la Section 6 ci-dessous, car son propre jeton ne se trouve sur le rayon d’aucune pièce d’échec.
4.4 Porte AND (corrigée)
Voir la Section 6 pour l’erreur trouvée dans la version initialement spécifiée de ce gadget et la Section 7 pour la conception corrigée : une Tour entièrement scellée (les quatre directions latérales et la direction « à contresens » murées) avec exactement un jeton bloquant adjacent, présent ssi NOT(xa AND xb). Cette conception ne se généralise à plus de deux entrées qu’en imbriquant des instances d’elle-même (un AND de AND), non en enchaînant plusieurs jetons le long de la propre ligne d’une porte ; voir Section 7.2.
4.5 Fusible de synchronisation des tempos
Là où deux couloirs alimentant le même point dans l’ordre d’alternance ont des longueurs naturelles différentes (nombre de coups d’avancée forcés avant leur point de branchement), le couloir le plus court est complété par des cases d’avancée forcée supplémentaires (ascension bloquée, comme à la Section 4.1) de sorte que les deux couloirs atteignent leur point de branchement après le même nombre de coups. Cela préserve la stricte alternance des coups entre les deux joueurs à travers des couloirs parallèles de longueur autrement inégale.
4.6 Gadget de condition de victoire
Une Tour V se trouve au seul point du plateau où sa propre ligne de rangée croise un rayon triagonal vers le Roi — le même rayon qu’occupe déjà une Licorne d’échec désignée, placée plus loin sur ce rayon avec un chemin dégagé. Les quatre directions latérales de V et sa direction « à contresens » sont scellées en permanence ; sa seule direction restante contient exactement un jeton bloquant adjacent (Section 7.1), présent ssi la formule globale est Fausse. Si V dispose d’un coup légal — ce qui, étant donné le scellement, se produit si et seulement si la formule est Vraie — jouer ce coup libère la case de départ de V, découvrant l’échec de la Licorne le long du rayon désormais dégagé, droit vers le Roi.
4.6.1 Sécurité du roi
Les six directions de case de fuite tridimensionnelles restantes du Roi (sur sa pleine mobilité à 26 voisins, moins la direction le long du rayon triagonal utilisé ci-dessus) sont scellées avec du matériel bloquant ordinaire (Pions, Tours, Fous se défendant mutuellement selon les besoins), indépendamment de la formule, de sorte que la seule manière dont la position du Roi passe de « sûr, une case de fuite » à « échec et mat, zéro case de fuite et en échec » est via le mécanisme du §4.6, qui est conditionné par la valeur de vérité de la formule et rien d’autre.
5. Correction, gadget par gadget
Nous énonçons la propriété de correction dont chaque gadget est responsable. Celles-ci sont énoncées au niveau de rigueur qu’un évaluateur pair devrait s’attendre à pouvoir vérifier par inspection de la construction et, là où existe une vérification informatique, à confirmer en outre que l’affirmation tenait sur les instances contrôlées ; elles ne sont pas revendiquées comme des preuves formelles vérifiées par machine.
5.1 (Couloir de variable). Pour chaque variable xi, le Pion de couloir dispose d’exactement un coup légal à chaque case avant la dernière (forcé, non informatif quant à xi), et d’exactement deux coups légaux à la dernière case, dont les destinations se distinguent purement par le fait que la destination partage ou non le niveau du couloir avec l’origine (Faux) ou non (Vrai). Vérifié informatiquement pour des longueurs de couloir allant jusqu’à 3 avec remplissage de fusible, Section 9.
5.2 (Porte OR). Le jeton OR dispose d’un coup légal si et seulement si au moins un jeton de négation d’entrée est absent. Vérifié informatiquement pour toutes les combinaisons d’entrée jusqu’à 4 entrées (deux instances indépendantes à 2 entrées alimentant une troisième porte), Section 9.
5.3 (Porte AND, corrigée). Le jeton AND dispose d’un coup légal si et seulement si le bloqueur adjacent est absent, ce qui est câblé pour se produire si et seulement si les deux entrées sont Vraies. Ceci n’est pas une affirmation sur une chaîne de jetons indépendamment mobiles (que la Section 6 montre être fausse) ; c’est une affirmation sur la présence ou l’absence d’un jeton unique, une propriété plus simple et, nous le croyons, désormais correctement énoncée. Vérifié informatiquement pour toutes les combinaisons allant jusqu’à 6 variables composées à travers 4 instances de porte, Section 9.
5.4 (Composition). Des instances de porte distinctes occupent des cases de plateau disjointes et des lignes infinies disjointes (axes de tour, diagonales de fou, triagonales de licorne) sauf là où une connexion est intentionnelle (p. ex., la sortie d’une porte OR câblée au bloqueur d’une porte AND), vérifié mécaniquement via un registre de collision de coordonnées (Section 9.1) plutôt que par inspection manuelle. Nous considérons ce registre, et non la relecture humaine, comme la norme de preuve appropriée pour cette affirmation spécifique, puisque la propre erreur de la Note 15 est née exactement du type de coïncidence accidentelle que le registre est construit pour détecter.
5.5 (Condition de victoire). V dispose d’un coup légal si et seulement si la valeur de formule câblée est Vraie, et jouer ce coup produit un véritable échec et mat (Roi en échec, zéro réponse légale), confirmé contre le générateur de coups légaux plutôt que supposé à partir de la description géométrique du gadget. Vérifié informatiquement pour l’exemple traité de la Section 9.3.
6. Une erreur trouvée, et ce qu’elle enseigne
La construction de porte AND initialement proposée (Section 6 de l’article consolidé, avant la correction du présent article) enchaînait plusieurs jetons booléens indépendamment mobiles directement le long de la propre ligne de rangée de V, sur le raisonnement que la retraite de V n’est légale qu’une fois chaque jeton libéré. Une vérification mécanique, utilisant le même générateur de coups légaux sur lequel s’appuie l’ensemble de ce projet, a montré cela faux : le rayon de la Licorne d’échec est découvert à l’instant où V quitte sa case de départ, pour quelque raison que ce soit et vers quelque destination que ce soit — non seulement en atteignant une case spécifique, entièrement repliée. Par conséquent, seul le jeton le plus proche de V compte : une fois qu’il se libère, V dispose d’un coup légal indépendamment de l’état de tout jeton plus loin sur la ligne, et le mat suit indépendamment. La construction, telle que spécifiée, calculait quelque chose de plus proche d’un OR que de l’AND revendiqué. Les détails complets, y compris le cas qui isole ceci de tout artefact de placement, sont consignés dans la Note technique no 15 de l’IRF.
Nous rapportons ceci non simplement comme un erratum mais parce que cela illustre un danger propre à ce style de construction : des gadgets construits autour d’une seule pièce physique servant simultanément d’élément computationnel (ici, une chaîne de bloqueurs de ligne de rangée) et de composante du mécanisme de délivrance du mat (se trouvant sur le rayon d’une pièce donnant échec) sont validés, par un contrôle proxy incomplet, d’une manière qui paraît solide jusqu’à ce que le mécanisme de mat lui-même soit vérifié directement et en combinaison. Chaque test de ce projet antérieur à celui ayant trouvé cette erreur vérifiait l’accessibilité d’une case spécifique plutôt que la véritable condition de victoire (V dispose-t-elle d’un quelconque coup légal) ; les deux ne coïncident que dans le cas à entrée unique. Nous considérons ceci comme une mise en garde pour les évaluateurs de ce style de construction en général, non uniquement pour ce gadget spécifique.
7. La construction corrigée
7.1 Un jeton, entièrement scellé
La réparation (Sections 4.4, 4.6) restreint V, et toute porte AND construite sur le même principe, à exactement un jeton bloquant adjacent, toutes les autres directions — y compris la direction « à contresens » le long du propre axe de la porte — étant scellées en permanence. Ce cas a été directement reconfirmé solide : jeton présent implique zéro coup légal ; jeton absent implique exactement un coup légal, dont l’exécution produit un échec et mat confirmé (pour V spécifiquement) ou le signal logique voulu (pour une porte AND intérieure).
7.2 Composition par découplage, non par partage
Les formules multi-variables sont traitées en calculant la valeur de chaque sous-formule à l’aide de portes construites entièrement sur des coordonnées disjointes de V et de tout rayon de pièce donnant échec, de sorte qu’aucun mouvement de jeton propre à une sous-porte ne puisse lui-même déclencher un échec par découverte, et en câblant la valeur résultante dans l’unique bloqueur adjacent de la porte suivante en remontant l’arbre (finalement, celui de V). Un AND de plus de deux entrées est réalisé en imbriquant des instances de porte AND (un AND de AND), non en ajoutant des jetons à la ligne d’une seule porte.
Cette réparation a un coût réel, énoncé franchement plutôt que minimisé : il n’est plus vrai qu’une seule pièce physique puisse servir un triple rôle en tant que propre jeton mobile d’une sous-formule, bloqueur de ligne de rangée, et pièce sur le rayon d’échec, simultanément, de la manière que la construction originale envisageait et que le travail de vérification propre à ce projet supposait sans vérification à un stade antérieur (avant la Note 15). La composition requiert désormais une étape de câblage explicite entre une sous-formule vérifiée et l’unique jeton qui compte pour la porte suivante. Qu’il existe une construction récupérant la composition à jeton unique sans câblage, sans réintroduire le défaut de la Section 6, demeure, à notre connaissance, ouvert.
8. Ce qui est établi et ce qui ne l’est pas
Nous jugeons important, pour un document destiné à l’évaluation par les pairs, d’être sans ambiguïté sur ce point.
Établi, au sens de vérifié mécaniquement sur des instances finies : la propriété de correction énoncée de chaque gadget individuel (Section 5), pour les tailles d’instance spécifiques testées ; l’absence de collision de coordonnées pour les instances assemblées spécifiques testées ; et, pour un exemple à six variables entièrement traité avec un jeu alterné réel et deux couloirs synchronisés en tempo, que le pipeline complet — couloirs, portes, composition, condition de victoire — produit une valeur minimax correspondant au raisonnement théorique des jeux indépendant sur cette formule, avec la position finale de la ligne gagnante confirmée comme un véritable échec et mat contre le générateur.
Non établi : une preuve générale, paramétrique en taille (p. ex., par induction sur la structure de la formule) que la construction est correcte pour tout n arbitraire, toute profondeur d’imbrication arbitraire, et toute partition variable-joueur arbitraire ; un compte rendu formel de toutes les règles de Raumschach non exercées par les gadgets tels que construits (prises interagissant avec le matériel de gadget au-delà de ce qu’anticipent les propres murs de chaque gadget, promotion, toute interaction avec la règle de triple répétition ou des cinquante coups, et subtilités de pièce défendue au-delà de l’argument de sécurité du Roi du §4.6.1) ; une preuve formelle vérifiée par machine ou à la main au sens qu’exigerait un théoricien de la complexité pour un théorème de difficulté prêt pour publication ; et une borne formelle reliant la taille de la formule à la taille de plateau construite n (nécessaire pour confirmer que la réduction est authentiquement en temps polynomial, non simplement d’apparence polynomiale sur les instances essayées).
Nous décrivons donc l’affirmation globale de cet article comme : un ensemble de gadgets corrigé qui survit à chaque contrôle que nous avons pu exécuter contre un générateur indépendant, présenté avec ces contrôles, à l’appui d’un résultat conjectural d’EXPTIME-difficulté pour Raumschach que nous n’avons pas encore prouvé en général.
9. Méthodologie de vérification informatique
9.1 Registre de collision de coordonnées
Chaque instance de gadget déclare les cases de plateau qu’elle occupe et, pour chaque pièce mobile, les lignes infinies (axe de tour, famille de plans diagonaux de fou, famille triagonale de licorne) le long desquelles elle pourrait en principe glisser. Un registre vérifie, à mesure que chaque gadget est ajouté à un assemblage, s’il partage une case ou une ligne avec tout gadget précédemment ajouté auquel il n’a pas explicitement déclaré une connexion intentionnelle. Ce contrôle est statique (géométrique), indépendant de la légalité des coups, et spécifiquement conçu pour détecter la classe d’erreur — deux gadgets individuellement corrects coïncidant par coïncidence de coordonnées — que ce projet a rencontrée plus d’une fois dans des gadgets construits avant l’existence du registre.
9.2 Générateur de coups légaux
Un générateur de coups indépendant (coups glissants de Tour, Fou, Licorne, Dame ; pas et sécurité du Roi ; avancée à un pas et ascension du Pion) est utilisé pour vérifier directement chaque affirmation de gadget : ensembles de coups légaux à des positions spécifiques, statut d’échec/échec et mat du Roi via square_attacked_by et énumération complète des coups de Roi, et, pour l’exemple composé, une recherche complète par induction rétrograde sur chaque demi-coup de branchement réel.
9.3 Exemple traité
La formule φ = (OR(x1,x2) AND OR(x3,x4)) OR AND(x5,x6), six variables, le Joueur A contrôlant x1,x4,x5 et le Joueur B contrôlant x2,x3,x6, a été assemblée avec le couloir de x1 à longueur naturelle 3 et celui de x2 à longueur naturelle 1 complété par un fusible à 2 coups, tous deux confirmés atteindre leur point de branchement en synchronisation après exactement 3 coups forcés chacun, entrelacés coup par coup. L’induction rétrograde complète sur l’arbre de jeu résultant à 64 feuilles a trouvé que A dispose d’un gain forcé (φ = Vrai sous jeu optimal), ce qui correspond au raisonnement indépendant : A contrôle une variable dans chaque clause OR du premier disjoint de la formule et peut forcer les deux clauses à Vrai unilatéralement, indépendamment de tout choix disponible pour B. La position terminale de la ligne gagnante a été confirmée comme un authentique échec et mat — Roi en échec, zéro réponse légale — contre le générateur, non supposée à partir de la géométrie de la construction.
10. Travaux connexes
Fraenkel et Lichtenstein (1981) ont établi le résultat fondateur dont descend l’affirmation de complexité cible de cet article, y compris l’obstacle de croisement de fils que l’usage d’une troisième dimension spatiale par cet article vise à contourner. Nous n’avons connaissance d’aucun travail antérieur appliquant cette observation spécifique à Raumschach ; l’article consolidé que ce document remplace en partie (Section 6) représente la propre tentative antérieure de ce projet, corrigée ici.
11. Conclusion
Nous avons présenté un ensemble de gadgets pour réduire un jeu de formule booléenne alternée à la détermination du vainqueur d’une position de Raumschach, corrigé une véritable erreur de validité trouvée lors de la vérification mécanique (documentée séparément dans la Note technique 15), et vérifié informatiquement la construction corrigée sur des instances allant jusqu’à six variables avec un jeu alterné réel et un échec et mat confirmé. Nous considérons les gadgets individuels et leur composition comme bien étayés par cette vérification, et nous considérons la preuve générale de correction pour un n arbitraire, ainsi qu’un compte rendu complet des règles de Raumschach au-delà de ce qu’exercent les gadgets, comme un travail ouvert. Nous soumettons cet article dans cet esprit : comme une esquisse rigoureuse et honnêtement délimitée pour évaluation, non comme un résultat clos.
Références
- Fraenkel, A. S., & Lichtenstein, D. (1981). Computing a perfect strategy for n×n chess requires time exponential in n. Journal of Combinatorial Theory, Series A, 31(2), 199–214.
- Fédération Internationale de Raumschach. (2026). Raumschach et complexité computationnelle : espace d’états, taille de l’arbre de jeu, et esquisse d’EXPTIME-difficulté. complexity-of-raumschach.html (analyse de l’espace d’états et de la taille de l’arbre de jeu non affectée par cet article ; Section 6 remplacée conformément à la Note technique 15).
- Fédération Internationale de Raumschach. (2026). Note technique no 15 de l’IRF : la porte AND qui ne filtre pas. technical-notes-15.html (l’erreur corrigée aux Sections 6–7 de cet article, en détail complet).
- Fédération Internationale de Raumschach. (2026). Notes techniques de l’IRF, nos 1–14 (journal de développement interne précédant l’article consolidé ; non publié séparément).
- Maack, F. (1907). Raumschach (description originale de la variante 5×5×5).