Toward EXPTIME-Hardness of Raumschach: A Verified Gadget Construction
A candidate reduction from Generalized Geography, with mechanically-checked gadget correctness — submitted for peer review
1. Introduction
Fraenkel and Lichtenstein’s classical result (1981) shows that deciding the winner of an n×n generalized chess position requires time exponential in n under any fixed algorithm, via a reduction from a PSPACE-hard alternating formula game played on a planar graph. A persistent technical obstacle in that construction, and in subsequent work extending it, is that the reduction’s control-flow graph is not planar in general, forcing an explicit “wire-crossing” gadget to route one logical signal over another on a two-dimensional board.
Raumschach, the 5×5×5 three-dimensional chess variant devised by Ferdinand Maack (1907), removes this obstacle for a structural reason: a board with a genuine third spatial dimension admits two corridors that do not share a plane, so crossing is not a special case requiring its own gadget — it is simply two disjoint paths. This paper develops that observation into a candidate reduction and reports, in full, both the reduction’s current state and an error found and corrected in the process of checking it.
This work follows a development arc recorded internally in IRF Technical Notes 1–15 (Notes 1–14 retained as an institutional record, not separately published) and the consolidated paper Raumschach and Computational Complexity, which this paper supersedes with respect to the win-condition/AND-gate construction specifically (Section 6 of that paper), per the erratum in Technical Note 15, which is published. Readers wanting the state-space and game-tree-size analysis, which is unaffected by anything in this paper, should consult that paper directly.
What this paper is, and is not. This is a technical report describing a reduction sketch, a set of gadgets, and a program of computational verification of those gadgets on finite instances — including one fully worked nontrivial example with six Boolean variables, real alternating play, and confirmed checkmate. It is not a completed, general mathematical proof that the reduction is correct for arbitrary formula size, and we do not claim EXPTIME-hardness as an established theorem here. We describe exactly where the gap between “verified on instances we checked” and “proven for all instances” currently sits, in Section 8.
2. Preliminaries
2.1 Raumschach
Raumschach is played on a 5×5×5 board, coordinates (L, f, r) ∈ {1,…,5}3 in the standard notation (level, file, rank). Pieces include the usual Rook, Bishop, Queen, King, and Pawn, plus the Unicorn, which moves along pure triagonal rays — all three coordinates changing by ±1 each step. For the reduction, we work on an enlarged n×n×n board, n polynomial in formula size, following the standard practice in this line of work of using an oversized board to embed a reduction and then arguing the construction respects whatever piece set and movement rules the base game defines.
2.2 The Source Problem
We reduce from a two-player, alternating-move formula game in the style of Generalized Geography / QBF-game formulations used in Fraenkel–Lichtenstein-type constructions: a Boolean formula φ(x1,…,xn) in some fixed basis (here, AND and OR suffice, by De Morgan’s law and the availability of a real NOT via mover assignment — see Section 7), together with a partition of the variables between two players, Player A and Player B, and a fixed order in which they are set. Player A wins if the resulting assignment satisfies φ; Player B wins otherwise. Deciding which player has a winning strategy for such games is PSPACE-complete in general, and the chess-reduction literature further composes this with board size considerations to obtain EXPTIME-hardness for the decision problem on suitably-sized boards. We do not re-derive that general complexity-theoretic backbone here; we take it as the target and focus on the board-level reduction.
2.3 What a Correct Reduction Must Do
A reduction from this game to Raumschach position-winner-determination must exhibit, for every formula φ and variable partition/order, a Raumschach position such that: (a) the position can be constructed in time polynomial in |φ|; (b) the two players’ moves in the resulting chess game correspond exactly to their choices of variable assignment, in the same order; and (c) White (WLOG, the player representing A) has a forced win in the chess game if and only if A has a winning strategy in the formula game. Every gadget in Section 4 exists to make some piece of this correspondence hold; Section 5 states, gadget by gadget, which piece it is responsible for.
3. Reduction Overview
The board is divided into disjoint regions: one region per formula variable (a corridor terminating in a binary branch point, per Section 4.1), one region per logical connective in the formula’s parse tree (an OR-gate or AND-gate instance, Section 4.3–4.4), tempo-matching fuse padding wherever two corridors of different natural length feed the same point in the alternation order (Section 4.5), and a single win-condition gadget (Section 4.6) whose own legality is wired — not shared-square-composed, see Section 5.4 — to the formula’s final truth value. King safety is established once, independent of the formula (Section 4.6.1), using six of a King’s seven three-dimensional flight-square directions sealed by ordinary blocking material and the seventh left open specifically to be closed by the win-condition gadget’s own discovered-check mechanism.
4. Gadgets
4.1 Variable Corridor
Each variable xi controlled by a given player is represented by a Pawn confined to a single file, advancing one square per move (Raumschach Pawns, like their two-dimensional counterpart, move exactly one square forward per non-capturing move), with ascent (the Pawn’s second single-step move type, changing level by one) blocked by an immobile Rook at every square along the corridor except the final one. At the final square, both the forward advance and the ascent are left open: ascent represents xi = True (the Pawn leaves the corridor’s level entirely), continued forward advance represents xi = False. This is a real, single-choice binary branch, resolved by an actual move against the actual legal-move generator, not a value assumed in advance.
4.2 Level-Crossing Via
Where a signal path in the formula’s parse tree would, on a two-dimensional board, need to cross another such path, Raumschach’s third dimension is used directly: the crossing path is routed through an adjacent level, with a level-changing Pawn ascent (or Bishop/Unicorn step, depending on the corridor’s piece type) serving as the “via.” No dedicated crossing gadget of the kind Fraenkel–Lichtenstein’s planar construction requires is needed; two corridors on different levels simply do not intersect.
4.3 OR-Gate
A single Rook token is given exactly two live rook directions, each independently walled by a negation-token: present (blocking) if the corresponding input is False, absent if True. The other four directions are permanently walled. The token has a legal move if and only if at least one of its two gated directions is open, i.e. if and only if at least one input is True — realizing OR. This gadget is unchanged from Section 7 of the consolidated paper and is not affected by the error described in Section 6 below, because its own token does not sit on any checking piece’s ray.
4.4 AND-Gate (Corrected)
See Section 6 for the error found in the originally-specified version of this gadget and Section 7 for the corrected design: a fully-sealed Rook (all four side directions and the “wrong-way” direction walled) with exactly one adjacent blocking token, present iff NOT(xa AND xb). This design generalizes to more than two inputs only by nesting instances of itself (an AND of ANDs), not by chaining multiple tokens along one gate’s own line; see Section 7.2.
4.5 Tempo-Matching Fuse
Where two corridors feeding the same point in the alternation order have different natural lengths (number of forced advance moves before their branch point), the shorter corridor is padded with additional forced-advance squares (ascent blocked, as in Section 4.1) so that both corridors reach their branch point after the same number of moves. This preserves strict move alternation between the two players across parallel corridors of otherwise-mismatched length.
4.6 Win-Condition Gadget
A Rook V sits at the one board point where its own rank line intersects a triagonal ray to the King — the same ray a designated checking Unicorn, placed further out on that ray with a clear path, already occupies. V’s four side directions and its “wrong-way” direction are permanently sealed; its one remaining direction holds exactly one adjacent blocking token (Section 7.1), present iff the overall formula is False. If V has a legal move — which, given the sealing, occurs if and only if the formula is True — making that move vacates V’s home square, discovering check from the Unicorn along the now-clear ray straight to the King.
4.6.1 King Safety
The King’s remaining six three-dimensional flight-square directions (of its full 26-neighbor mobility, minus the one direction along the triagonal ray used above) are sealed with ordinary blocking material (Pawns, Rooks, Bishops defending each other as needed), independent of the formula, so that the only way the King’s position changes from “safe, one flight square” to “checkmated, zero flight squares and in check” is via the mechanism in 4.6, which is gated by the formula’s truth value and nothing else.
5. Correctness, Gadget by Gadget
We state the correctness property each gadget is responsible for. These are stated at the level of rigor a peer reviewer should expect to be able to check by inspection of the construction and, where computational verification exists, to additionally confirm the claim held on the checked instances; they are not claimed as machine-checked formal proofs.
5.1 (Variable corridor). For each variable xi, the corridor Pawn has exactly one legal move at every square before the final one (forced, uninformative with respect to xi), and exactly two legal moves at the final square, whose destinations are distinguishable purely by whether the destination shares the corridor’s level with the origin (False) or not (True). Verified computationally for corridor lengths up to 3 with fuse padding, Section 9.
5.2 (OR-gate). The OR token has a legal move if and only if at least one input negation-token is absent. Verified computationally for all input combinations up to 4 inputs (two independent 2-input instances feeding a third gate), Section 9.
5.3 (AND-gate, corrected). The AND token has a legal move if and only if the adjacent blocker is absent, which is wired to occur if and only if both inputs are True. This is not a claim about a chain of independently-movable tokens (which Section 6 shows to be false); it is a claim about a single token’s presence or absence, which is a simpler and, we believe, now correctly stated property. Verified computationally for all combinations of up to 6 composed variables through 4 gate instances, Section 9.
5.4 (Composition). Distinct gate instances occupy disjoint board cells and disjoint infinite lines (rook axes, bishop diagonals, unicorn triagonals) except where a connection is intentional (e.g., an OR-gate’s output wired to an AND-gate’s blocker), checked mechanically via a coordinate-collision registry (Section 9.1) rather than by hand inspection. We consider this registry, and not human proofreading, the appropriate standard of evidence for this specific claim, since Note 15’s own error arose from exactly the kind of accidental coincidence the registry is built to catch.
5.5 (Win condition). V has a legal move if and only if the wired formula value is True, and making that move produces actual checkmate (King in check, zero legal replies), confirmed against the legal-move generator rather than assumed from the gadget’s geometric description. Verified computationally for the worked example of Section 9.3.
6. An Error Found, and What It Teaches
The AND-gate construction originally proposed (Section 6 of the consolidated paper, prior to this paper’s correction) chained multiple independently-movable Boolean tokens directly along V’s own rank line, on the reasoning that V’s retreat is legal only once every token has vacated. Mechanical checking, using the same legal-move generator relied on throughout this project, found this false: the checking Unicorn’s ray is discovered the instant V leaves its home square, for any reason and to any destination — not only upon reaching a specific, fully-retreated square. Consequently only the token nearest V matters: once it vacates, V has some legal move regardless of the state of any token further down the line, and mate follows regardless. The construction, as specified, computed something closer to OR than to the claimed AND. Full details, including the case that isolates this from any placement artifact, are recorded in IRF Technical Note 15.
We report this not merely as an erratum but because it illustrates a hazard specific to this style of construction: gadgets built around a single physical piece serving simultaneously as a computational element (here, a rank-line blocker chain) and as a component of the mate-delivery mechanism (sitting on a checking piece’s ray) are validated, by an incomplete proxy check, in a way that looks sound until the mate mechanism itself is checked directly and in combination. Every test in this project prior to the one that found this error checked reachability of one specific square rather than the real win condition (does V have any legal move at all); the two coincide only in the single-input case. We regard this as a caution for reviewers of this style of construction generally, not only for this specific gadget.
7. The Corrected Construction
7.1 One Token, Fully Sealed
The repair (Section 4.4, 4.6) restricts V, and any AND-gate built on the same principle, to exactly one adjacent blocking token, with all other directions — including the “wrong way” direction along the gate’s own axis — permanently sealed. This case was directly reconfirmed sound: token present implies zero legal moves; token absent implies exactly one legal move, whose execution produces confirmed checkmate (for V specifically) or the intended logical signal (for an interior AND-gate).
7.2 Composition by Decoupling, Not by Sharing
Multi-variable formulas are handled by computing every sub-formula’s value using gates built entirely on coordinates disjoint from V and from any checking piece’s ray, so that no sub-gate’s own token movement can itself trigger a discovered check, and wiring the resulting value into the single adjacent blocker of the next gate up the tree (ultimately, of V). An AND of more than two inputs is realized by nesting AND-gate instances (an AND of ANDs), not by adding tokens to one gate’s line.
This repair has a real cost, stated plainly rather than minimized: it is no longer the case that one physical piece can serve triple duty as a sub-formula’s own mobile token, a rank-line blocker, and a piece on the checking ray, simultaneously, the way the original construction envisioned and the way an earlier stage of this project’s own verification work (before Note 15) assumed without checking. Composition now requires an explicit wiring step between a verified sub-formula and the one token that matters for the next gate up. Whether a construction recovering single-token, no-wiring composition exists without reintroducing Section 6’s flaw is, to our knowledge, open.
8. What Is Established and What Is Not
We think it important, for a document intended for peer review, to be unambiguous about this.
Established, in the sense of mechanically checked on finite instances: each individual gadget’s stated correctness property (Section 5), for the specific instance sizes tested; freedom from coordinate collision for the specific assembled instances tested; and, for one worked six-variable formula with real alternating play and two tempo-matched corridors, that the full pipeline — corridors, gates, composition, win condition — produces a minimax value matching independent game-theoretic reasoning about that formula, with the winning line’s final position confirmed as actual checkmate against the generator.
Not established: a general, size-parametric proof (e.g., by induction on formula structure) that the construction is correct for arbitrary n, arbitrary nesting depth, and arbitrary variable-to-mover partition; a formal accounting of all Raumschach rules not exercised by the gadgets as built (captures interacting with gadget material beyond what each gadget’s own walls anticipate, promotion, any threefold-repetition or fifty-move-rule interaction, and defended-piece subtleties beyond the King-safety argument of 4.6.1); a machine-checked or hand-checked formal proof in the sense a complexity theorist would require for a journal-ready hardness theorem; and a formal bound relating formula size to constructed board size n (needed to confirm the reduction is genuinely polynomial-time, not merely polynomial-looking on the instances tried).
We describe the overall claim of this paper, accordingly, as: a corrected gadget set that survives every check we have been able to run against an independent generator, presented together with those checks, in support of a conjectured EXPTIME-hardness result for Raumschach that we have not yet proven in general.
9. Computational Verification Methodology
9.1 Coordinate-Collision Registry
Every gadget instance declares the board cells it occupies and, for each mobile piece, the infinite lines (rook axis, bishop diagonal-plane-family, unicorn triagonal-family) it could in principle slide along. A registry checks, as each gadget is added to an assembly, whether it shares a cell or line with any previously-added gadget it has not explicitly declared an intentional connection to. This check is static (geometric), independent of move legality, and is specifically designed to catch the class of error — two independently-correct gadgets coinciding by coordinate coincidence — that this project has encountered more than once in gadgets built before the registry existed.
9.2 Legal-Move Generator
An independent move generator (Rook, Bishop, Unicorn, Queen sliding moves; King step-and-safety; Pawn single-step advance and ascent) is used to check every gadget claim directly: legal move sets at specific positions, King check/checkmate status via square_attacked_by and full King-move enumeration, and, for the composed example, a full backward-induction search over every real branching ply.
9.3 Worked Example
The formula φ = (OR(x1,x2) AND OR(x3,x4)) OR AND(x5,x6), six variables, Player A controlling x1,x4,x5 and Player B controlling x2,x3,x6, was assembled with x1’s corridor at natural length 3 and x2’s at natural length 1 padded with a 2-move fuse, both confirmed to reach their branch point in sync after exactly 3 forced moves each, interleaved turn-by-turn. Full backward induction over the resulting 64-leaf game tree found A has a forced win (φ = True under best play), which matches independent reasoning: A controls one variable in each OR clause of the formula’s first disjunct and can force both clauses True unilaterally, regardless of any choice available to B. The winning line’s terminal position was confirmed as genuine checkmate — King in check, zero legal replies — against the generator, not assumed from the construction’s geometry.
10. Related Work
Fraenkel and Lichtenstein (1981) established the foundational result this paper’s target complexity claim descends from, including the wire-crossing obstacle this paper’s use of a third spatial dimension is intended to sidestep. We are not aware of prior work applying this specific observation to Raumschach; the consolidated paper this document supersedes in part (Section 6) represents this project’s own earlier attempt, corrected here.
11. Conclusion
We have presented a gadget set for reducing an alternating Boolean formula game to Raumschach position-winner-determination, corrected a genuine soundness error found during mechanical verification (documented separately in Technical Note 15), and verified the corrected construction computationally on instances up to six variables with real alternating play and confirmed checkmate. We consider the individual gadgets and their composition well-supported by this checking, and we consider the general, arbitrary-n correctness proof, along with a full accounting of Raumschach’s rules beyond what the gadgets exercise, to be open work. We submit this paper in that spirit: as a rigorous, honestly-scoped sketch for review, not as a closed result.
References
- 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 (state-space and game-tree-size analysis unaffected by this paper; Section 6 superseded per Technical Note 15).
- International Raumschach Federation. (2026). IRF Technical Note No. 15: The AND-Gate Does Not Gate. technical-notes-15.html (the error corrected in Sections 6–7 of this paper, in full detail).
- International Raumschach Federation. (2026). IRF Technical Notes, Nos. 1–14 (internal development log preceding the consolidated paper; not separately published).
- Maack, F. (1907). Raumschach (original description of the 5×5×5 variant).