Solving Sokoban Backward — Provable Dead Squares via Pull-BFS, and a Push-Optimal BFS Solver

typescript dev.to

Sokoban, built for the browser with two real algorithms inside. (1) Static dead-square proofs — think backward: a box can reach a goal iff the goal can reach the box by pulling, and pulls have no deadlocks, so one reverse BFS from the goals marks every provably-dead square before any search (toggle the overlay in the demo). (2) A push-optimal BFS whose state is the box set plus the player's reachable region, so the first solution found has the fewest pushes. All six bundled levels are solver-verified — and the test suite actually caught one of my levels being genuinely impossible. Solver-equipped puzzle #4, after Sudoku (#33), Lights Out (#284), and the 15-puzzle (#285).

🌐 Live demo: https://sen.ltd/portfolio/sokoban/
📦 GitHub: https://github.com/sen-ltd/sokoban

Dead squares: think backward

Forward reasoning asks "where can this box go?" — expensive. The trick is to
reason backward: a box can reach a goal iff the goal can be reached by
pulling the box, and pulls have no deadlocks. One BFS from every goal,
expanding by legal pulls, marks every alive square:

// a pull from `from` to `to` needs the player standing beyond `to`
const to = from + d;
const playerSq = to + d;
if (walls[to] || walls[playerSq]) continue;   // otherwise `to` is pull-reachable
Enter fullscreen mode Exit fullscreen mode

Everything unmarked is a dead square: push a box there and the level is
provably lost — no search needed. Non-goal corners fall out automatically, and
so do entire goal-less wall edges (pinned by a test). The solver prunes pushes
onto dead squares outright, and the demo renders them red with a checkbox.

The solver: push-optimal BFS over (region, boxes)

Between pushes the player only walks, so the exact position doesn't matter —
only which region the player can reach. A search state is the box set plus the
player's reachable region, canonicalized to its smallest cell:

const k = canon + ':' + boxes.join(',');   // state key: region + box set
Enter fullscreen mode Exit fullscreen mode

Transitions are single pushes (the player must reach the cell behind the box).
BFS depth = number of pushes, so the first solution found is push-optimal.
The status line reports pushes, states, and time — the screenshot shows a
6-push optimum found in 648 states / 11 ms.

A detail I like: solve runs from the current position. Shove a box into a
corner, hit Solve, and it answers "provably unsolvable from here — try Undo".
The state space was exhausted, not timed out — a proof, not a guess.

For animation, each push expands into player steps via a per-push BFS walk
(expandSolution), and a test replays every step through the movement rules to
confirm legality and a final win.

Ship levels through your solver

The six bundled mini-levels are original, and the tests demand the solver solve
every one with a replay-verified result. While designing them, I wrote a
level where boxes sat against the right wall — structurally impossible to ever
push left. Genuinely unsolvable, instantly flagged by the suite, redesigned.
Lesson: your level editor is not done until your solver signs off.

src/sokoban.ts      — pure engine: parser, movement, pull-BFS dead squares,
                      push-optimal BFS, walk pathing, solution expansion
src/sokoban.test.ts — 17 cases (rules, dead squares, solver proofs, replays)
src/levels.ts       — 6 original levels, all solver-verified
src/main.ts         — DOM shell: grid, input, undo, animated solve, dead overlay
Enter fullscreen mode Exit fullscreen mode

Takeaway

Sokoban rewards combining forward search with backward proof: pull-BFS
settles impossibility before the search starts, and BFS over (region, box-set)
returns push-optimal solutions. That makes four solver-equipped puzzles — Sudoku,
Lights Out (GF(2)), the 15-puzzle (parity + IDA*), and Sokoban (pull-BFS +
push-optimal BFS) — each wearing a different piece of mathematics.

🌐 Live demo: https://sen.ltd/portfolio/sokoban/
📦 GitHub: https://github.com/sen-ltd/sokoban

Source: dev.to

arrow_back Back to Tutorials