Every board is provable, or it doesn't ship

How KEEPYBOO guarantees “no guessing” · 2026-10-07

Minesweeper has a famous flaw. Sooner or later a board hands you a 50/50 and your win depends on a coin flip, not on your reasoning. KEEPYBOO is a small logic puzzle built by one person in Japan around a single promise: no board ever asks you to guess. This post explains how that promise is kept, how we measure how deep a board's reasoning goes, and what it cost to compute.

The puzzle

A board is an n×n grid (5×5 up to 9×9) with hidden ghosts. Three kinds of numbers tell you where they are:

a number at the head of a row or column says how many ghosts that line holds,
a number inside a cell says how many ghosts are in the 8 cells around it (that cell itself never holds a ghost),
that's it. There is no separate “total ghosts” rule; the row numbers already add up to the total.

You tap once to mark a cell as empty (×), double-tap to catch a ghost. Three lives. The largest shipped board is 9×9 with 36 ghosts.

A 6 by 6 KEEPYBOO board with column counts on top, row counts on the left, nine clue cells, two ghosts already found in the bottom row and the empty first column marked with crosses — ROUND 217, a 6×6 board, after the first two waves of single-condition moves: the first column's count is 0, so it is all ×; the bottom row has two blanks left for two ghosts.

So it is Minesweeper's neighbour-count rule plus Nonogram-style line counts, with everything visible from the start. There is no “click to reveal” and therefore no first-click lottery.

What “no guessing” means here, precisely

“Solvable by logic” is vague unless you say which logic. We define three rule layers, and a board ships only if a program using only those rules finds every ghost without ever being wrong.

Layer 1, one condition at a time. Each row, column and clue cell is a condition: a set of cells and a target count. If a condition already has all its ghosts, every other cell in it is ×. If its remaining blanks exactly equal the ghosts still missing, they are all ghosts.

Layer 2, two conditions at a time. Take two conditions A and B that overlap. Split their blank cells into A-only, B-only and the common part C. The number of ghosts in C is bounded:

lo = max(0, a − |A-only|, b − |B-only|)
hi = min(a, b, |C|)

where a and b are the ghosts still missing in A and B. If lo = hi, the common part is decided, and that often decides A-only or B-only too. This is the “subset” or “interval” reasoning that experienced Minesweeper players do by eye.

Layer 3, one assumption. Assume one cell is a ghost (or empty), propagate layers 1 and 2 to a fixed point (at most 64 steps), and if that leads to a contradiction, the opposite is proven. This is proof by contradiction, limited to one assumption at a time.

That limit is deliberate. We experimented with nesting assumptions, and rejected it: with enough nesting every cell of every board becomes “provable”, and the word stops meaning anything to a player. A second level (one case split inside the assumption, with a budget of 400 propagations) exists in the code, but it runs only in a background check described below, never in the shipping test.

The same board with column 3 outlined in blue and the 3 by 3 neighbourhood of the 2-clue outlined in orange; their two shared cells are marked C, and the arithmetic below shows lo and hi both equal to 1 — The same board, at the point where single conditions run dry. Column 3 still needs one ghost; the 2-clue in the top row still needs two. Their two shared cells must hold exactly one ghost, which settles a cell in each condition.

How boards are made

Nothing is generated on the phone. All 2,000 rounds are generated offline and shipped as a 1.26 MB JSON asset.

The generator is plain rejection sampling. For each board size it picks a ghost count and a clue count inside a band (5×5: 4–7 ghosts, 9×9: 18–26 for the standard sets), places them at random, and discards the board unless the layer-1 solver alone clears it within a target number of “waves”. A wave is one pass that applies every move currently available. It also throws away boards with more than three zero-conditions, because those give too much away for free. Each size gets up to 600 attempts per wanted board, and the survivors are bucketed by wave count to build a difficulty staircase.

The harder sets are generated differently on purpose. One generator produces boards that require layer 2, and boards that require exactly one contradiction. That is how the paid EXTREME and ULTIMATE sets get their character (“overlap constraint chains” and “contradiction networks”) instead of just being bigger.

Two safety nets sit under all of this:

The solver is run against the stored solution during generation. If any deduction ever disagrees with the solution, the board is thrown out. A board that the rules clear completely is also unique by construction: there is never a point where two solutions remain.
A separate audit replays every one of the 2,000 rounds, greedily catching only ghosts that are provable under layers 1–3 from confirmed information. The current result: 2,000 measured, 0 unsolved.

Honesty note: the oldest 1,000 rounds come from an earlier browser prototype and carry their own metadata (unique: true, plus deduction counts). They pass the same audit as everything else, which is why we trust them.

Measuring how deep the reasoning goes

Board size is a poor difficulty measure. A 9×9 can be a warm-up and a 7×7 can be nasty. We wanted a number that reflects how much reasoning a board demands, not how many cells it has.

The measure, logicDepth, is computed by playing each round with the real game engine the way a careful player would: at every step apply every move available in the lowest layer that has any. Count the waves per layer, then

logicDepth = direct + 2·pair + 2·contradiction

The weights 2 and 2 were not guessed. We grid-searched {2,3,4,6,8}² and kept the pair that made the tier medians monotone with the most even steps between tiers. Results across the 2,000 rounds:

	Rounds needing it	Max waves
Layer 1 only	969	11
Layer 2 (pairs)	1,031	8
Layer 3 (one contradiction)	293	13

Tier medians of logicDepth run 3 / 3 / 4 / 5 / 7 / 9.5 / 10 / 12 / 14 / 19.5 from EASY to ULTIMATE+. The deepest board shipped has depth 43. EASY boards never need a pair; everything from EXTREME II up always does; ULTIMATE needs a contradiction on 73 of its 150 boards.

Box plots of logic depth for the ten tiers from EASY to ULTIMATE plus; medians rise from 3 to 19.5 and the maximum is 43 — Logic depth of all 2,000 rounds by tier. The box is the middle half of the rounds, the orange line the median, the whiskers the minimum and maximum.

A rating that uses the depth

With a difficulty number per board you can rate players the way exam questions rate students. KEEPYBOO's “Logic Rating” is a one-parameter Rasch model: the chance a player of ability θ clears a board of depth b cleanly is

P = 1 / (1 + exp(−a (θ − b)))

A clean clear means first attempt, no hints, and every ghost caught was provable at the moment you caught it (the game checks this on every tap and marks the round 🧠 only if it holds; a lucky guess loses the mark). θ is fitted by Newton's method with a mild prior, shown ×100 on a 0–4,400 scale, appears after 20 attempts and is called “settled” after 60. The slope a = 0.3 is provisional; we'll re-fit it once there is enough data, and we say so in the code.

Because every tap is judged against confirmed information only (your pencil marks don't count), the 🧠 mark is a statement about your reasoning, not about the outcome.

The expensive part: the best and worst possible score

Each catch scores 100 + 50 × (cells opened) × (conditions completed at once), so the order in which you find ghosts matters. We wanted two trophies: 💎 for a no-miss clear that reaches the proven maximum score, and 💀 for being held down to the proven minimum.

“Proven” is the hard word. The maximum over all discovery orders is a subset dynamic program over 2^G states for G ghosts. In C with combinatorial indexing, G = 33 takes 18 minutes; G = 34 takes 35; the three G = 36 boards took 198–257 minutes each on 14 cores with about 33 GiB of RAM. All 1,658 values computed by the earlier, slower version were reproduced exactly by the new one.

On top of that we compute, for every round, which ghosts are “free”: ghosts you can catch at any point along a maximum-score path without losing the maximum. That is another pass over the same state space (about 20–25 hours for the full set). About 40% of ghosts turn out to be free; five rounds have none. The result is folded into a reduced decision diagram per board (one table of 200k rows became 265 nodes and 1,074 bytes), so the whole thing ships as a 296 KB asset, and the phone only ever does lookups.

What we didn't do, and why

No on-device generation. Random boards would be cheap, but we couldn't promise “no guessing” for them, and we couldn't precompute the trophies.
No deeper proof in the shipping test. Nested assumptions make everything provable and make 🧠 meaningless.
No timer, no daily streak pressure, no friend leaderboard. The point of a puzzle you can always reason through is that you get to take your time.

The game is free (1,110 rounds), with two paid sets for people who want the contradiction-network boards. It is on iOS and Android, in 14 languages, and this October every player can pick up a Halloween sound set.

If you've built a solver or a generator with a different notion of “no guessing”, I'd genuinely like to compare notes. The question of which logic counts is the interesting part.

Written by the developer. Contact: contact@keepyboo.com · About KEEPYBOO