Auf dem Weg zur EXPTIME-Härte von Raumschach: Eine verifizierte Gadget-Konstruktion

Eine Kandidaten-Reduktion von Generalized Geography, mit mechanisch geprüfter Gadget-Korrektheit — zur Begutachtung eingereicht

International Raumschach Federation  ·  2026  ·  ersetzt Abschnitt 6 von Raumschach und Berechnungskomplexität, gemäß IRF Technical Note Nr. 15

1. Einführung

Das klassische Ergebnis von Fraenkel und Lichtenstein (1981) zeigt, dass die Bestimmung des Gewinners einer verallgemeinerten (n×n)-Schachstellung unter jedem festen Algorithmus Zeit exponentiell in n erfordert, mittels einer Reduktion von einem PSPACE-harten alternierenden Formelspiel, das auf einem planaren Graphen gespielt wird. Ein anhaltendes technisches Hindernis in jener Konstruktion, und in nachfolgenden Arbeiten, die sie erweitern, besteht darin, dass der Kontrollflussgraph der Reduktion im Allgemeinen nicht planar ist, was ein explizites „Leitungskreuzungs“-Gadget erzwingt, um ein logisches Signal über ein anderes auf einem zweidimensionalen Brett zu führen.

Raumschach, die von Ferdinand Maack (1907) erdachte dreidimensionale Schachvariante auf einem 5×5×5-Brett, beseitigt dieses Hindernis aus strukturellen Gründen: Ein Brett mit einer echten dritten räumlichen Dimension erlaubt zwei Korridore, die keine Ebene teilen, sodass eine Kreuzung kein Sonderfall ist, der ein eigenes Gadget erfordert — sie ist schlicht zwei disjunkte Pfade. Dieses Papier entwickelt diese Beobachtung zu einer Kandidaten-Reduktion und berichtet vollständig sowohl vom aktuellen Stand der Reduktion als auch von einem Fehler, der beim Prüfen gefunden und korrigiert wurde.

Diese Arbeit folgt einem Entwicklungsbogen, der intern in den IRF Technical Notes 1–15 festgehalten ist (Notes 1–14 als institutionelles Protokoll aufbewahrt, nicht gesondert veröffentlicht) sowie im konsolidierten Papier Raumschach und Berechnungskomplexität, das dieses Papier speziell hinsichtlich der Konstruktion des Gewinnbedingungs-/UND-Gatters ersetzt (Abschnitt 6 jenes Papiers), gemäß dem Erratum in Technical Note 15, das veröffentlicht ist. Leser, die die Zustandsraum- und Spielbaumgrößenanalyse suchen, die von nichts in diesem Papier betroffen ist, sollten jenes Papier direkt konsultieren.

Was dieses Papier ist, und was nicht. Dies ist ein technischer Bericht, der eine Reduktionsskizze, eine Reihe von Gadgets und ein Programm rechnerischer Verifikation dieser Gadgets an endlichen Instanzen beschreibt — einschließlich eines vollständig ausgearbeiteten nichttrivialen Beispiels mit sechs Booleschen Variablen, echtem alternierendem Spiel und bestätigtem Schachmatt. Es ist kein vollständiger, allgemeiner mathematischer Beweis, dass die Reduktion für beliebige Formelgrößen korrekt ist, und wir beanspruchen EXPTIME-Härte hier nicht als etabliertes Theorem. Wir beschreiben in Abschnitt 8 genau, wo die Lücke zwischen „auf geprüften Instanzen verifiziert“ und „für alle Instanzen bewiesen“ derzeit liegt.

2. Grundlagen

2.1 Raumschach

Raumschach wird auf einem 5×5×5-Brett gespielt, mit Koordinaten (E, L, R) ∈ {1,…,5}³ in der Standardnotation (Ebene, Linie, Reihe). Zu den Figuren zählen der übliche Turm, Läufer, Dame, König und Bauer, sowie das Einhorn, das sich entlang reiner Triagonalstrahlen bewegt — alle drei Koordinaten ändern sich bei jedem Schritt um ±1. Für die Reduktion arbeiten wir auf einem vergrößerten n×n×n-Brett, mit n polynomial in der Formelgröße, gemäß der in dieser Forschungsrichtung üblichen Praxis, ein überdimensioniertes Brett zu verwenden, um eine Reduktion einzubetten, und dann zu argumentieren, dass die Konstruktion den Figurensatz und die Bewegungsregeln respektiert, die das Basisspiel definiert.

2.2 Das Ausgangsproblem

Wir reduzieren von einem alternierenden Zwei-Spieler-Formelspiel im Stil der Generalized-Geography-/QBF-Spielformulierungen, die in Konstruktionen vom Fraenkel-Lichtenstein-Typ verwendet werden: eine Boolesche Formel φ(x₁,…,x_n) in einer festen Basis (hier genügen UND und ODER, dank des De-Morgan'schen Gesetzes und der Verfügbarkeit eines echten NICHT über die Spielerzuordnung — siehe Abschnitt 7), zusammen mit einer Aufteilung der Variablen zwischen zwei Spielern, Spieler A und Spieler B, und einer festen Reihenfolge, in der sie gesetzt werden. Spieler A gewinnt, wenn die resultierende Zuweisung φ erfüllt; andernfalls gewinnt Spieler B. Zu bestimmen, welcher Spieler eine Gewinnstrategie für solche Spiele hat, ist im Allgemeinen PSPACE-vollständig, und die Literatur zu Schachreduktionen kombiniert dies weiter mit Überlegungen zur Brettgröße, um EXPTIME-Härte für das Entscheidungsproblem auf geeignet dimensionierten Brettern zu erhalten. Wir leiten dieses allgemeine komplexitätstheoretische Grundgerüst hier nicht neu her; wir nehmen es als Zielgröße und konzentrieren uns auf die Reduktion auf Brettebene.

2.3 Was eine korrekte Reduktion leisten muss

Eine Reduktion von diesem Spiel auf die Bestimmung des Raumschach-Stellungsgewinners muss für jede Formel φ und jede Variablenaufteilung/-reihenfolge eine Raumschach-Stellung liefern, sodass gilt: (a) Die Stellung lässt sich in Zeit polynomial in |φ| konstruieren; (b) die Züge der beiden Spieler im resultierenden Schachspiel entsprechen genau ihren Entscheidungen zur Variablenzuweisung, in derselben Reihenfolge; und (c) Weiß (o.B.d.A. der Spieler, der A repräsentiert) hat genau dann einen erzwungenen Gewinn im Schachspiel, wenn A eine Gewinnstrategie im Formelspiel hat. Jedes Gadget in Abschnitt 4 existiert, um einen Teil dieser Entsprechung sicherzustellen; Abschnitt 5 gibt Gadget für Gadget an, für welchen Teil es verantwortlich ist.

3. Überblick über die Reduktion

Das Brett ist in disjunkte Regionen unterteilt: eine Region pro Formelvariable (ein Korridor, der in einem binären Verzweigungspunkt endet, gemäß Abschnitt 4.1), eine Region pro logischem Verknüpfungssymbol im Parsebaum der Formel (eine ODER-Gatter- oder UND-Gatter-Instanz, Abschnitte 4.3–4.4), Taktabgleich-Zünderpolsterung überall dort, wo zwei Korridore unterschiedlicher natürlicher Länge denselben Punkt in der Alternierungsreihenfolge speisen (Abschnitt 4.5), sowie ein einzelnes Gewinnbedingungs-Gadget (Abschnitt 4.6), dessen eigene Legalität — verdrahtet, nicht durch gemeinsame Felder zusammengesetzt, siehe Abschnitt 5.4 — an den endgültigen Wahrheitswert der Formel gekoppelt ist. Königssicherheit wird einmalig hergestellt, unabhängig von der Formel (Abschnitt 4.6.1), indem sechs der sieben dreidimensionalen Fluchtfeldrichtungen des Königs durch gewöhnliches Blockmaterial versiegelt werden und die siebte offen bleibt, eigens dazu bestimmt, durch den eigenen Abzugsschach-Mechanismus des Gewinnbedingungs-Gadgets geschlossen zu werden.

4. Gadgets

4.1 Variablenkorridor

Jede von einem gegebenen Spieler kontrollierte Variable x_i wird durch einen Bauern dargestellt, der auf eine einzige Linie beschränkt ist und sich pro Zug um ein Feld vorwärtsbewegt (Raumschach-Bauern ziehen, wie ihr zweidimensionales Gegenstück, bei einem nicht schlagenden Zug genau ein Feld vorwärts), wobei der Aufstieg (die zweite Einzelschritt-Zugart des Bauern, die die Ebene um eins ändert) an jedem Feld entlang des Korridors außer dem letzten durch einen unbeweglichen Turm blockiert ist. Am letzten Feld sind sowohl der Vorwärtszug als auch der Aufstieg offen: Der Aufstieg stellt x_i = Wahr dar (der Bauer verlässt die Ebene des Korridors vollständig), der fortgesetzte Vorwärtszug stellt x_i = Falsch dar. Dies ist eine echte, einmalige binäre Verzweigung, die durch einen tatsächlichen Zug gegen den tatsächlichen Generator für legale Züge aufgelöst wird, nicht ein im Voraus angenommener Wert.

4.2 Ebenenübergang

Wo ein Signalpfad im Parsebaum der Formel auf einem zweidimensionalen Brett einen anderen solchen Pfad kreuzen müsste, wird Raumschachs dritte Dimension direkt genutzt: Der kreuzende Pfad wird durch eine benachbarte Ebene geführt, wobei ein ebenenwechselnder Bauernaufstieg (oder ein Läufer-/Einhornschritt, je nach Figurentyp des Korridors) als „Übergang“ dient. Es ist kein eigenes Kreuzungs-Gadget nötig, wie es die planare Konstruktion von Fraenkel und Lichtenstein erfordert; zwei Korridore auf unterschiedlichen Ebenen schneiden sich schlicht nicht.

4.3 ODER-Gatter

Ein einzelner Turm-Token erhält genau zwei aktive Turmrichtungen, jede unabhängig durch einen Negations-Token ummauert: anwesend (blockierend), wenn die entsprechende Eingabe Falsch ist, abwesend, wenn Wahr. Die übrigen vier Richtungen sind dauerhaft ummauert. Der Token hat genau dann einen legalen Zug, wenn mindestens eine seiner beiden gegatterten Richtungen offen ist, das heißt genau dann, wenn mindestens eine Eingabe Wahr ist — dies realisiert ODER. Dieses Gadget ist gegenüber Abschnitt 7 des konsolidierten Papiers unverändert und ist vom in Abschnitt 6 unten beschriebenen Fehler nicht betroffen, da sein eigener Token nicht auf dem Strahl einer schachbietenden Figur sitzt.

4.4 UND-Gatter (korrigiert)

Siehe Abschnitt 6 für den in der ursprünglich spezifizierten Version dieses Gadgets gefundenen Fehler und Abschnitt 7 für den korrigierten Entwurf: ein vollständig versiegelter Turm (alle vier Seitenrichtungen sowie die „falsche“ Richtung ummauert) mit genau einem benachbarten Blockade-Token, anwesend genau dann, wenn NICHT(x_a UND x_b). Dieser Entwurf verallgemeinert sich auf mehr als zwei Eingaben nur durch Verschachtelung von Instanzen seiner selbst (ein UND von UNDs), nicht durch Verkettung mehrerer Token entlang der eigenen Linie eines Gatters; siehe Abschnitt 7.2.

4.5 Taktabgleich-Zünder

Wo zwei Korridore, die denselben Punkt in der Alternierungsreihenfolge speisen, unterschiedliche natürliche Längen haben (Anzahl der erzwungenen Vorwärtszüge vor ihrem Verzweigungspunkt), wird der kürzere Korridor mit zusätzlichen erzwungenen Vorwärtsfeldern gepolstert (Aufstieg blockiert, wie in Abschnitt 4.1), sodass beide Korridore ihren Verzweigungspunkt nach derselben Anzahl von Zügen erreichen. Dies bewahrt die strikte Zugalternation zwischen den beiden Spielern über parallele Korridore unterschiedlicher Länge hinweg.

4.6 Gewinnbedingungs-Gadget

Ein Turm V sitzt an dem einen Brettpunkt, an dem seine eigene Reihenlinie einen Triagonalstrahl zum König schneidet — denselben Strahl, den ein designiertes schachbietendes Einhorn, weiter außen auf diesem Strahl mit freier Bahn platziert, bereits besetzt. Vs vier Seitenrichtungen und seine „falsche“ Richtung sind dauerhaft versiegelt; seine eine verbleibende Richtung enthält genau einen benachbarten Blockade-Token (Abschnitt 7.1), anwesend genau dann, wenn die Gesamtformel Falsch ist. Hat V einen legalen Zug — was angesichts der Versiegelung genau dann eintritt, wenn die Formel Wahr ist —, räumt das Ausführen dieses Zuges Vs Heimatfeld und deckt Schach durch das Einhorn entlang des nun freien Strahls direkt zum König auf.

4.6.1 Königssicherheit

Die verbleibenden sechs dreidimensionalen Fluchtfeldrichtungen des Königs (von seiner vollen 26-Felder-Mobilität, abzüglich der oben verwendeten Richtung entlang des Triagonalstrahls) sind mit gewöhnlichem Blockmaterial versiegelt (Bauern, Türme, sich gegenseitig deckende Läufer nach Bedarf), unabhängig von der Formel, sodass sich die Stellung des Königs nur über den in 4.6 beschriebenen Mechanismus von „sicher, ein Fluchtfeld“ zu „matt gesetzt, null Fluchtfelder und im Schach“ ändern kann — ein Mechanismus, der ausschließlich vom Wahrheitswert der Formel gesteuert wird.

5. Korrektheit, Gadget für Gadget

Wir formulieren die Korrektheitseigenschaft, für die jedes Gadget verantwortlich ist. Diese sind auf dem Rigor-Niveau formuliert, das ein Gutachter durch Prüfung der Konstruktion nachvollziehen können sollte, und, wo rechnerische Verifikation vorliegt, zusätzlich bestätigen kann, dass die Behauptung auf den geprüften Instanzen zutraf; sie werden nicht als maschinell geprüfte formale Beweise beansprucht.

5.1 (Variablenkorridor). Für jede Variable x_i hat der Korridor-Bauer an jedem Feld vor dem letzten genau einen legalen Zug (erzwungen, bezüglich x_i uninformativ), und am letzten Feld genau zwei legale Züge, deren Zielfelder sich rein danach unterscheiden lassen, ob das Zielfeld die Ebene des Korridors mit dem Ursprungsfeld teilt (Falsch) oder nicht (Wahr). Rechnerisch verifiziert für Korridorlängen bis 3 mit Zünderpolsterung, Abschnitt 9.

5.2 (ODER-Gatter). Der ODER-Token hat genau dann einen legalen Zug, wenn mindestens ein Eingabe-Negations-Token abwesend ist. Rechnerisch verifiziert für alle Eingabekombinationen bis zu 4 Eingaben (zwei unabhängige 2-Eingaben-Instanzen, die ein drittes Gatter speisen), Abschnitt 9.

5.3 (UND-Gatter, korrigiert). Der UND-Token hat genau dann einen legalen Zug, wenn der benachbarte Blocker abwesend ist, was so verdrahtet ist, dass dies genau dann eintritt, wenn beide Eingaben Wahr sind. Dies ist keine Behauptung über eine Kette unabhängig beweglicher Token (was Abschnitt 6 als falsch erweist); es ist eine Behauptung über die Anwesenheit oder Abwesenheit eines einzelnen Tokens, was eine einfachere und, wie wir meinen, nun korrekt formulierte Eigenschaft ist. Rechnerisch verifiziert für alle Kombinationen von bis zu 6 zusammengesetzten Variablen über 4 Gatter-Instanzen, Abschnitt 9.

5.4 (Zusammensetzung). Verschiedene Gatter-Instanzen belegen disjunkte Brettfelder und disjunkte unendliche Linien (Turmachsen, Läuferdiagonalen, Einhorn-Triagonalen), außer wo eine Verbindung beabsichtigt ist (z. B. der Ausgang eines ODER-Gatters, verdrahtet zum Blocker eines UND-Gatters), mechanisch geprüft über ein Koordinaten-Kollisionsregister (Abschnitt 9.1) statt durch manuelle Prüfung. Wir betrachten dieses Register, und nicht menschliches Korrekturlesen, als den angemessenen Evidenzstandard für diese spezifische Behauptung, da der Fehler aus Note 15 genau aus der Art zufälliger Koinzidenz entstand, die das Register aufzudecken bestimmt ist.

5.5 (Gewinnbedingung). V hat genau dann einen legalen Zug, wenn der verdrahtete Formelwert Wahr ist, und die Ausführung dieses Zuges erzeugt tatsächliches Schachmatt (König im Schach, null legale Erwiderungen), bestätigt gegen den Generator für legale Züge statt aus der geometrischen Beschreibung des Gadgets angenommen. Rechnerisch verifiziert für das ausgearbeitete Beispiel aus Abschnitt 9.3.

6. Ein gefundener Fehler, und was er lehrt

Die ursprünglich vorgeschlagene UND-Gatter-Konstruktion (Abschnitt 6 des konsolidierten Papiers, vor der Korrektur in diesem Papier) verkettete mehrere unabhängig bewegliche Boolesche Token direkt entlang Vs eigener Reihenlinie, mit der Begründung, dass Vs Rückzug erst legal sei, sobald jeder Token das Feld geräumt habe. Mechanische Prüfung, unter Verwendung desselben Generators für legale Züge, auf den sich dieses Projekt durchgehend stützt, erwies dies als falsch: Der Strahl des schachbietenden Einhorns wird in dem Moment aufgedeckt, in dem V sein Heimatfeld verlässt, aus jedem Grund und zu jedem Zielfeld — nicht nur beim Erreichen eines bestimmten, vollständig zurückgezogenen Feldes. Folglich zählt nur der V nächstgelegene Token: Sobald dieser das Feld räumt, hat V irgendeinen legalen Zug, unabhängig vom Zustand jedes weiter entfernten Tokens, und Matt folgt in jedem Fall. Die Konstruktion berechnete, wie spezifiziert, etwas, das eher ODER als dem behaupteten UND entsprach. Vollständige Details, einschließlich des Falls, der dies von jedem Platzierungsartefakt isoliert, sind in IRF Technical Note 15 festgehalten.

Wir berichten davon nicht bloß als Errata, sondern weil es eine Gefahr veranschaulicht, die dieser Art von Konstruktion eigen ist: Gadgets, die um eine einzelne physische Figur herum aufgebaut sind, die zugleich als Rechenelement (hier: eine Blockade-Kette auf der Reihenlinie) und als Bestandteil des Mattlieferungsmechanismus (auf dem Strahl einer schachbietenden Figur sitzend) dient, werden durch eine unvollständige Ersatzprüfung validiert, auf eine Weise, die solide erscheint, bis der Mattmechanismus selbst direkt und in Kombination geprüft wird. Jeder Test in diesem Projekt vor demjenigen, der diesen Fehler fand, prüfte die Erreichbarkeit eines bestimmten Feldes statt der eigentlichen Gewinnbedingung (hat V überhaupt irgendeinen legalen Zug); beide fallen nur im Einzeleingabe-Fall zusammen. Wir betrachten dies als eine Warnung für Gutachter dieser Art von Konstruktion im Allgemeinen, nicht nur für dieses spezifische Gadget.

7. Die korrigierte Konstruktion

7.1 Ein Token, vollständig versiegelt

Die Reparatur (Abschnitt 4.4, 4.6) beschränkt V, und jedes UND-Gatter, das nach demselben Prinzip aufgebaut ist, auf genau einen benachbarten Blockade-Token, wobei alle anderen Richtungen — einschließlich der „falschen“ Richtung entlang der eigenen Achse des Gatters — dauerhaft versiegelt sind. Dieser Fall wurde direkt als solide bestätigt: Anwesenheit des Tokens impliziert null legale Züge; Abwesenheit des Tokens impliziert genau einen legalen Zug, dessen Ausführung bestätigtes Schachmatt (speziell für V) oder das beabsichtigte logische Signal (für ein inneres UND-Gatter) erzeugt.

7.2 Zusammensetzung durch Entkopplung, nicht durch gemeinsame Nutzung

Mehrvariablige Formeln werden behandelt, indem der Wert jeder Teilformel mit Gattern berechnet wird, die vollständig auf Koordinaten aufgebaut sind, die disjunkt von V und vom Strahl jeder schachbietenden Figur sind, sodass die eigene Token-Bewegung keines Untergatters selbst ein Abzugsschach auslösen kann, und indem der resultierende Wert in den einzigen benachbarten Blocker des nächsthöheren Gatters im Baum (letztlich von V) eingespeist wird. Ein UND von mehr als zwei Eingaben wird durch Verschachtelung von UND-Gatter-Instanzen realisiert (ein UND von UNDs), nicht durch Hinzufügen von Token zur Linie eines einzelnen Gatters.

Diese Reparatur hat echte Kosten, die wir offen benennen statt zu beschönigen: Es ist nicht mehr der Fall, dass eine einzelne physische Figur zugleich als eigener beweglicher Token einer Teilformel, als Blockade auf der Reihenlinie und als Figur auf dem schachbietenden Strahl dienen kann, wie es die ursprüngliche Konstruktion vorsah und wie eine frühere Phase der eigenen Verifikationsarbeit dieses Projekts (vor Note 15) ungeprüft annahm. Die Zusammensetzung erfordert nun einen expliziten Verdrahtungsschritt zwischen einer verifizierten Teilformel und dem einen Token, der für das nächsthöhere Gatter zählt. Ob eine Konstruktion existiert, die Einzeltoken-Zusammensetzung ohne Verdrahtung wiederherstellt, ohne den Fehler aus Abschnitt 6 erneut einzuführen, ist unseres Wissens offen.

8. Was etabliert ist und was nicht

Wir halten es für ein Dokument, das zur Begutachtung bestimmt ist, für wichtig, hierüber unmissverständlich zu sein.

Etabliert, im Sinne von mechanisch geprüft an endlichen Instanzen: die formulierte Korrektheitseigenschaft jedes einzelnen Gadgets (Abschnitt 5), für die spezifischen getesteten Instanzgrößen; Freiheit von Koordinatenkollisionen für die spezifischen getesteten zusammengesetzten Instanzen; und, für eine ausgearbeitete Sechs-Variablen-Formel mit echtem alternierendem Spiel und zwei taktabgleich-angepassten Korridoren, dass die vollständige Pipeline — Korridore, Gatter, Zusammensetzung, Gewinnbedingung — einen Minimax-Wert erzeugt, der mit unabhängiger spieltheoretischer Überlegung zu jener Formel übereinstimmt, wobei die Endstellung der Gewinnlinie als tatsächliches Schachmatt gegen den Generator bestätigt wurde.

Nicht etabliert: ein allgemeiner, größenparametrischer Beweis (z. B. durch Induktion über die Formelstruktur), dass die Konstruktion für beliebiges n, beliebige Verschachtelungstiefe und beliebige Variablen-Spieler-Zuordnung korrekt ist; eine formale Erfassung aller Raumschach-Regeln, die von den wie gebaut vorliegenden Gadgets nicht in Anspruch genommen werden (Schlagzüge, die mit Gadget-Material über das hinaus interagieren, was die eigenen Mauern jedes Gadgets vorsehen, Verwandlung, jede Interaktion mit der Dreifachwiederholungs- oder Fünfzig-Zug-Regel, sowie Feinheiten gedeckter Figuren über das Königssicherheitsargument aus 4.6.1 hinaus); ein maschinell oder handschriftlich geprüfter formaler Beweis im Sinne dessen, was ein Komplexitätstheoretiker für ein publikationsreifes Härtetheorem verlangen würde; sowie eine formale Schranke, die die Formelgröße mit der konstruierten Brettgröße n in Beziehung setzt (nötig, um zu bestätigen, dass die Reduktion tatsächlich polynomialzeitlich ist, nicht nur auf den getesteten Instanzen polynomial aussieht).

Wir beschreiben die Gesamtbehauptung dieses Papiers demgemäß als: eine korrigierte Gadget-Sammlung, die jede Prüfung übersteht, die wir gegen einen unabhängigen Generator durchführen konnten, präsentiert zusammen mit diesen Prüfungen, zur Stützung eines vermuteten EXPTIME-Härteergebnisses für Raumschach, das wir im Allgemeinen noch nicht bewiesen haben.

9. Methodik der rechnerischen Verifikation

9.1 Koordinaten-Kollisionsregister

Jede Gadget-Instanz deklariert die Brettfelder, die sie belegt, und für jede bewegliche Figur die unendlichen Linien (Turmachse, Läufer-Diagonalebenenfamilie, Einhorn-Triagonalfamilie), entlang derer sie sich im Prinzip bewegen könnte. Ein Register prüft bei jedem zu einer Zusammenstellung hinzugefügten Gadget, ob es ein Feld oder eine Linie mit einem zuvor hinzugefügten Gadget teilt, zu dem keine ausdrücklich beabsichtigte Verbindung erklärt wurde. Diese Prüfung ist statisch (geometrisch), unabhängig von der Zuglegalität, und speziell darauf ausgelegt, jene Fehlerklasse abzufangen — zwei für sich genommen korrekte Gadgets, die durch koordinatenmäßigen Zufall zusammenfallen —, auf die dieses Projekt bei Gadgets, die vor der Existenz des Registers gebaut wurden, mehr als einmal gestoßen ist.

9.2 Generator für legale Züge

Ein unabhängiger Zuggenerator (gleitende Züge für Turm, Läufer, Einhorn, Dame; Königsschritt und -sicherheit; Bauernvorwärtszug und -aufstieg als Einzelschritte) wird verwendet, um jede Gadget-Behauptung direkt zu prüfen: legale Zugmengen an bestimmten Stellungen, König-Schach-/Mattstatus über square_attacked_by und vollständige Aufzählung der Königszüge, sowie, für das zusammengesetzte Beispiel, eine vollständige Rückwärtsinduktionssuche über jeden tatsächlichen verzweigenden Halbzug.

9.3 Ausgearbeitetes Beispiel

Die Formel φ = (ODER(x₁,x₂) UND ODER(x₃,x₄)) ODER UND(x₅,x₆), sechs Variablen, wobei Spieler A x₁,x₄,x₅ kontrolliert und Spieler B x₂,x₃,x₆, wurde zusammengestellt, mit dem Korridor von x₁ in natürlicher Länge 3 und dem von x₂ in natürlicher Länge 1, aufgepolstert mit einem 2-Zug-Zünder, beide bestätigt, ihren Verzweigungspunkt nach jeweils genau 3 erzwungenen Zügen synchron zu erreichen, Zug um Zug verschränkt. Vollständige Rückwärtsinduktion über den resultierenden Spielbaum mit 64 Blättern ergab, dass A einen erzwungenen Gewinn hat (φ = Wahr bei bestem Spiel), was mit unabhängiger Überlegung übereinstimmt: A kontrolliert eine Variable in jeder ODER-Klausel der ersten Disjunktion der Formel und kann beide Klauseln einseitig auf Wahr erzwingen, unabhängig von jeder B zur Verfügung stehenden Wahl. Die Endstellung der Gewinnlinie wurde als echtes Schachmatt bestätigt — König im Schach, null legale Erwiderungen — gegen den Generator, nicht aus der Geometrie der Konstruktion angenommen.

10. Verwandte Arbeiten

Fraenkel und Lichtenstein (1981) etablierten das grundlegende Ergebnis, von dem die Zielkomplexitätsbehauptung dieses Papiers abstammt, einschließlich des Leitungskreuzungshindernisses, das die Nutzung einer dritten räumlichen Dimension in diesem Papier umgehen soll. Uns ist keine frühere Arbeit bekannt, die diese spezifische Beobachtung auf Raumschach anwendet; das konsolidierte Papier, das dieses Dokument teilweise ersetzt (Abschnitt 6), stellt den eigenen früheren Versuch dieses Projekts dar, hier korrigiert.

11. Schluss

Wir haben eine Gadget-Sammlung zur Reduktion eines alternierenden Booleschen Formelspiels auf die Bestimmung des Stellungsgewinners in Raumschach vorgelegt, einen echten Solidheitsfehler korrigiert, der während der mechanischen Verifikation gefunden wurde (gesondert dokumentiert in Technical Note 15), und die korrigierte Konstruktion rechnerisch an Instanzen mit bis zu sechs Variablen mit echtem alternierendem Spiel und bestätigtem Schachmatt verifiziert. Wir betrachten die einzelnen Gadgets und ihre Zusammensetzung durch diese Prüfung als gut gestützt, und wir betrachten den allgemeinen, für beliebiges n gültigen Korrektheitsbeweis, zusammen mit einer vollständigen Erfassung der Raumschach-Regeln über das von den Gadgets Beanspruchte hinaus, als offene Arbeit. Wir reichen dieses Papier in diesem Geist ein: als eine rigorose, ehrlich begrenzte Skizze zur Begutachtung, nicht als abgeschlossenes Ergebnis.

Literaturverzeichnis

• 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.
• International Raumschach Federation. (2026). Raumschach and Computational Complexity: State Space, Game-Tree Size, and an EXPTIME-Hardness Sketch. complexity-of-raumschach.html (Zustandsraum- und Spielbaumgrößenanalyse von diesem Papier unberührt; Abschnitt 6 gemäß Technical Note 15 ersetzt).
• International Raumschach Federation. (2026). IRF Technical Note No. 15: The AND-Gate Does Not Gate. technical-notes-15.html (der in den Abschnitten 6–7 dieses Papiers korrigierte Fehler, in vollem Detail).
• International Raumschach Federation. (2026). IRF Technical Notes, Nr. 1–14 (internes Entwicklungsprotokoll vor dem konsolidierten Papier; nicht gesondert veröffentlicht).
• Maack, F. (1907). Raumschach (ursprüngliche Beschreibung der 5×5×5-Variante).