sokoban: the fewest pushes, on hidden boards

A count-first project (PER-374). Agents improve a Sokoban solver (src/). Each held-out board is a warehouse of walls, boxes and goals; the solver returns the moves that put every box on a goal. The grader runs the solver itself, under an emulator that counts its instructions, gives each board the same budget of them, replays every solution under the rules, and scores its pushes over the board's optimum. mean_ratio, the mean over the boards, is minimised. It is exact and deterministic: one run decides a verification.

Sokoban is the classic hard planning puzzle (PSPACE-complete; Culberson 1997), and solving it in the fewest pushes is harder still. Two things make the usual benchmarks of it poor ones here, and this project is built around both:

• Public answers. The standard collections (XSokoban's 90, Microban, the Sasquatch sets) are online with their best known solutions: a solver could embed them. Here the boards are new, made by a seeded generator for this project, and the held-out ones are hidden.
• Time limits. "Solved within 60 s" depends on the machine and its load. Here the budget is a count of instructions, the same on every machine, and a solver that keeps to it solves the same way on every run.

File	What it is
autoresearch.toml	the metric (mean_ratio, minimised, MMI 1.5% relative, deterministic, epsilon 0), runner class cpu-s, editable src/**, K = 4; no upstream, public
PROGRAM.md	instructions for the agents: the solver, its budget, the rules, what counts as cheating
CONTRACT.md	the worker HTTP contract (the template's, plus this project's one item: the solver's files)
src/solver.py	the solver being improved: to start with, a greedy best-first search over pushes
harness/worker.py	the frozen worker: hands the grader src/'s files, and runs none of them
grader/grade.py, grader/driver.py, grader/sokoban.py	the grader, the driver it runs the solver with, and the rules it replays under
grader/measure.py	a solver's counts and pushes on a set, board by board, as the grader counts them (in the grader's image)
grader/sandbox.py, grader/native/	the instruction-count kit, release 2 (sdk/insncap/project verbatim)
grader/arh_grader	the grader SDK, release 6 (sdk/grader/src verbatim)
tools/boards.py	the generator that made the boards and proved their optima (offline; never run in a verification)
sample/items.jsonl	the public sample: 12 boards, with their optima and optimal solutions
dockerfile.worker, dockerfile.grader, compose.yaml	Python 3.13, standard library only; the grader builds QEMU and the kit's plugin from pinned sources
LICENSE	MIT

How a run is scored

/eval/items.jsonl holds the boards: on the platform the held-out set, projects/sokoban-heldout/ in the platform's repository; locally the public sample. Each line is {"board", "ref", "provenance"}.

1. The grader asks the worker for its solver ({"name": "solver"}) and gets src/'s files.
2. Its own Python runs grader/driver.py under QEMU's user-mode emulator with the instruction-count kit's plugin and sandbox (sdk/insncap in the platform's repository; the tree profile: the guest sees Python's standard library, the driver and the solver, nothing else). The driver imports the solver, then calls solve(board, budget) on each board in the file's order, {"board", "budget"} only: never ref. The emulator reports the count at each board's start, so the import and each board are counted apart.
3. Each solution is replayed under the rules (grader/sokoban.py; PROGRAM.md, "The rules").
4. A board over its budget (BUDGET, 10^9 instructions), an import over its own (IMPORT_BUDGET, 10^9), a solution the replay refuses, or no solution makes the run invalid (failures, by kind in failure_kinds).
5. Otherwise each board scores pushes / ref, divided exactly and rounded once to a float, and mean_ratio is their mean. The scores are the item scores (items.json). The secondary values are the instructions (all, the import's, the most any board took) and the pushes and moves, summed.

Nothing in a run depends on the host: the count is exact, the guest's clocks read the count (a nanosecond an instruction), its randomness is seeded, and its files are the same tree on every machine. Two runs of the same solver agree instruction for instruction.

Budget and time

The budget is 10^9 instructions a board: about a third of a second of native Python, and room for an A* of a few thousand states in plain Python, many more in a careful one. The incumbent takes 0.02 to 0.81 billion instructions a board on the held-out set (median 0.14 billion), 30.5 billion in all, and its import 22 million. Under the emulator Python runs at about 50 to 300 million instructions a second, depending on the host's load, so the incumbent's run takes a few minutes, and a solver that spends every board's whole budget about 2 x 10^11 instructions: 15 minutes to an hour. run_timeout_s is 7200 s, for a contended pool; build_timeout_s is 1800 s, for building the emulator.

The boards

The held-out set has 192 boards, the sample 12 others, all made by tools/boards.py: rooms of 10 x 10 with 5 boxes and 11 x 11 with 6 (each candidate's size drawn from its seed; the held-out set has 139 and 53, as the smaller rooms pass more often), from 20 to 42 pushes from solved (24 on average). The held-out boards come from a seed drawn with secrets and not kept; the sample's seed is 374 (python tools/boards.py candidates part.jsonl --seed 374 --first 0 --last 160, then pick sample/items.jsonl --count 12 part.jsonl).

The generator, after Taylor & Parberry (2011, "Procedural generation of Sokoban levels"), written here:

1. a room: floor carved by a seeded random walk inside a wall frame;
2. goals on its floor, a box on each;
3. a breadth-first search backwards from the solved boards, each step a pull: a board's depth in it is the fewest pulls that make it from a solved board, which is the fewest pushes that solve it;
4. the start is drawn from the deepest layer the search reaches.

A board is kept when the incumbent solves it within the budget, and when no kept board (or, for the held-out set, no sample board) is the same up to the square's 8 symmetries. So the boards are the part of the generator's space a greedy search can solve: hard to solve well, not hard to solve. The held-out set's 192 came from its first 1,632 candidates (12%).

References

A board's ref is its proven optimum, the fewest pushes that solve it: its depth in the generator's backward search, which visits every board in order of its distance from a solved one. Its record (provenance) holds the tool's version, the candidate's seed, the room's size and box count, the states the search reached, "optimal": true, and an optimal solution (solution), which the tests replay with the grader's own code to exactly ref pushes. Nothing can score below 1.0, and 1.0 on every board is the end of the project: a later reward version would add larger boards, where the optimum can't be proven, with best-known references.

The MMI

A step is 1.5% of the incumbent's mean_ratio. The metric is deterministic, so the floor is the held-out set's sampling error: twice the bootstrap standard error of the incumbent's item scores (arh_core.noise), 1.31% of its mean on the held-out set. The MMI is above it.

The incumbent

src/solver.py is a greedy best-first search over push states: the next state is the one whose boxes are nearest goals (the sum of each box's push distance to its nearest goal), pushes onto dead cells are never made, and it stops at the first solution. It keeps to its budget by counting states, budget // INSTRUCTIONS_PER_EXPANSION of them (3,000,000 instructions each, above the most an expansion took on any board measured, 2.4 million), so it solves the same way natively and under the grader. It scores mean_ratio 1.1077 on the held-out set (boards from 1.0 to 1.48, sd 0.10; 61 of the 192 optimal) and 1.0776 on the sample. About 10% of headroom to the optimum, 7 steps.

Running it

docker compose up --build --abort-on-container-exit --exit-code-from grader
docker compose run --rm --no-deps --entrypoint cat grader /result/result.json
docker compose down --volumes

arh run (the platform's CLI, cli/README.md) runs the same three commands and prints the result. A solver's counts board by board, in the grader's image:

docker run --rm -v "$PWD/src:/w/src:ro" -v "$PWD/sample:/w/set:ro" GRADER \
    python measure.py /w/src /w/set/items.jsonl

The project has no upstream ([project].upstream left out, ADR-0004). Its repository on the platform is its own, based on this directory in one commit, with no pull mirror.

Licences

What	Source	Licence
everything in this directory but the below	this project	MIT
QEMU 11.1.2, patched (grader/native/qemu.patch)	https://download.qemu.org, built from its release tarball in the grader's image, not vendored	GPL-2.0-only
Python 3.13 (python:3.13-slim-bookworm)	Docker Hub, the images' base	PSF-2.0