MULTI-HOP CAUSAL REASONING · FORMAL SAFETY GATING
Gen-Zero Sokoban: Multi-Hop Deadlock Invariant Proof
Every push is checked against two real invariants before it lands: a precomputed dead-square table and a recursive freeze-deadlock closure. Try the built-in levels, build your own trap in the editor, or let the solver break it.
- Gate decision latency
- —
- Deadlock intercepts
- 0
- Solver hops (last run)
- —
- Solver nodes explored
- —
- Token burn
- 0 tokens ($0.00)
- Pushes made
- 0
Keyboard: arrow keys or WASD. The gate blocks a push the instant it would create a proven dead-square or freeze; it never lets you walk into one, and never fakes a rescue.
What the gate actually checks
Dead-square table: a reverse-pull breadth-first search from every goal, computed once per level. Any floor cell it never reaches is proven unable to ever deliver a box to a goal — pushing a box there is refused.
Freeze closure: after every push, the moved box is checked recursively — a box is frozen if both its axes are pinned by a wall or by another box that is itself frozen. A 2×2 block of boxes, or a box wedged against an already-frozen neighbor, is caught this way even off the dead-square table.
Auto-Solve: a real breadth-first search over (player, box-set) states, capped at a node budget so it stays real-time in your browser. It reports the exact hop count and nodes explored — or says plainly that no solution was found within the budget. It never draws a path it did not find.