Chocona in the browser with four rule sets inside. Shade some
cells of an n×n grid: a region printed with a number contains exactly
that many shaded cells, and every orthogonally connected clump of
shaded cells is a filled rectangle. Clumps may cross region borders
and may touch at corners — only edge contact merges them. Puzzle #40 in
the solver series.
Demo: https://sen.ltd/portfolio/chocona/
Repo: https://github.com/sen-ltd/chocona
I picked this puzzle for two reasons.
A global law with an exact local double
"Every clump is a rectangle" sounds like a shape property you can only
check by looking at whole clumps. It is exactly equivalent to one local
test: no 2×2 window anywhere may contain exactly three shaded cells.
Zero, one, two or four are all legal; only three is banned. One direction
is easy — three cells in a 2×2 always form an L, and the L's bounding box
keeps a white cell no rectangle can swallow. The other direction — no
three-in-a-window anywhere implies every clump is a rectangle — is the
actual theorem.
The equivalence gives Chocona its signature backwards move. Most shading
puzzles have a no filled 2×2 rule, so a square about to complete gets
relieved with white. Chocona inverts it: three shaded cells in a square
force the fourth shaded, because the only escape from an L-corner is to
complete it.
The implementation deliberately splits the theorem across engines:
- the validator checks the definition itself — flood fill each clump, compare its size with its bounding-box area. It never looks at a 2×2 window;
- the rule ladder (
corner, below) reasons only through 2×2 windows; - the brute force prunes only with bounding boxes;
- the exhaustive anchor enumerates via a third formulation: a clump is rectangular iff every pair of its cells spans an all-shaded bounding box (also equivalent — a short corner-walking exercise to prove).
When engines built on different formulations agree on solution counts,
the test suite doubles as a machine check of the equivalence. Numbers
below.
Four rule sets
| level | rule |
|---|---|
quota |
region counts, both directions: number reached — rest white; free cells exactly the missing blacks — all black. Never crosses a region border alone |
corner |
the local double: no 2×2 window with exactly three blacks. Three blacks turn the fourth black; two blacks beside a decided white turn the last cell white |
box |
the rectangle law made global again: a clump's bounding box must fill; a clump with no feasible rectangle left (no white inside, no outside black touching the border) is a contradiction; a neighbor no feasible rectangle reaches must be white — the moat where the finished rectangle's border will run |
probe |
assume one color on one cell, run the rules below to a fixpoint, drop the assumption if that alone is a contradiction |
The raw stream carries almost no information
Measured on 300 raw generator boards per size — random partition (regions
up to 5 cells), random rectangle packing, every region numbered.
Fraction finished by the fixpoint alone, no guessing:
| board | quota | +corner | +box | +probe | unique answers in the raw stream |
|---|---|---|---|---|---|
| 6×6 | 0.0% | 0.3% | 0.3% | 1.0% | 1.0% |
| 8×8 | 0.0% | 0.0% | 0.0% | 0.3% | 0.3% |
| 10×10 | 0.0% | 0.0% | 0.0% | 0.0% | 0.0% |
The same table for the previous puzzle in this series, Aqre, read 21.3% at
6×6 and 7.7% at 8×8. The reason Chocona collapses is the sheer size of
its configuration space: the clue-free 2×2 / 3×3 / 4×4 boards already
have 12 / 208 / 10,148 legal shadings (Aqre: 14 / 219 / 798 — its
run rule constrains both colors, while Chocona's rectangle law never
penalizes not shading; the all-white board is legal at every size).
Print every number and the board still doesn't budge.
Ablation: equivalent laws are interchangeable propagators
Full ladder minus one rule, same boards:
| board | full | −quota | −corner | −box |
|---|---|---|---|---|
| 6×6 | 1.0% | 0.0% | 1.0% | 1.0% |
| 8×8 | 0.3% | 0.0% | 0.3% | 0.3% |
| 10×10 | 0.0% | 0.0% | 0.0% | 0.0% |
Dropping corner costs nothing. Dropping box costs nothing. Under
the probe, the local and the global formulation fully substitute for each
other — laws that are equivalent as laws turn out interchangeable as
propagators, which is the equivalence theorem wearing its operational
face. I expected corner ⊂ box; the surprise ran the other way too. While
writing tests I found the corner deduction I'd assumed was box-blind —
diagonal black pair plus one white forces the last window cell white —
rediscovered independently by the box rule's moat ("any rectangle over
the pair either swallows the white or touches the other black"). One
deduction, two proofs: the equivalence in miniature, sitting in a test
case.
Only quota, the one rule that reads the numbers, is irreplaceable.
Aqre's ablation collapsed on every removed rule; Chocona's redundancy
is structurally doubled instead — the same law written in two languages.
"Obviously," you might say. This series exists to check the obvious with
numbers.
The setter's dial has a cliff; the answer's dial has a slope
Partition granularity (the setter's dial), 8×8, 150 boards per point:
| maxSize | regions (mean) | unique | probe solves | quota-only solves |
|---|---|---|---|---|
| 1 | 64.0 | 100.0% | 100.0% | 100.0% |
| 2 | 45.9 | 2.7% | 2.7% | 0.0% |
| 3 | 35.9 | 0.0% | 0.0% | 0.0% |
| 5 | 25.8 | 0.0% | 0.0% | 0.0% |
| 8 | 18.4 | 0.0% | 0.0% | 0.0% |
| 12 | 13.5 | 0.0% | 0.0% | 0.0% |
Aqre's granularity dial swept a slope: 100% → 46% → 22% → 3.3%. Chocona's
is a cliff: 100% → 2.7% → 0.0%. One step coarser than
one-cell-regions (which just print the answer) and the information is
gone. The clue-density dial is outright dead — 0.0% unique at every
setting at 8×8, including full disclosure.
Instead, Chocona has something new for this series: a third dial,
owned by neither the partition nor the numbers. The rectangle scale
(maxRect) shapes the answer itself:
| maxRect | rects (mean) | black share (mean) | unique | probe solves |
|---|---|---|---|---|
| 1 | 23.4 | 36.5% | 0.0% | 0.0% |
| 2 | 13.0 | 35.9% | 0.0% | 0.0% |
| 3 | 9.1 | 37.6% | 0.0% | 0.0% |
| 4 | 7.0 | 41.6% | 0.7% | 0.7% |
| 5 | 5.8 | 41.6% | 1.3% | 1.3% |
A few large slabs carry more information than 1×1 confetti, at nearly the
same black share (36–42% across the row). The same amount of black,
arranged differently, changes how much a clue pins down.
The generator throws darts instead of searching
Chocona's legal configurations are exactly the packings of pairwise
non-edge-touching rectangles — so the generator doesn't search. It throws
2n² random rectangles at the grid and keeps each one whose cells and four
side strips are still free. Every dart lands or misses in O(area): no
backtracking, no heavy-tailed DFS, no restart cap. The pathology that
once hung Aqre's randomized-DFS generator for eight hours is
structurally impossible here. It's the cleanest application yet of this
series' lesson from Yin-Yang (where a bijection to a known combinatorial
object made sampling 9,000× faster): when legal boards correspond to
something you can construct directly, construct — don't search.
The bank: the middle is buildable, the top is scarce
The shipped bank covers 6×6 / 8×8 / 10×10 at four grades. In a world
where full-disclosure random partitions solve 0.0% of the time, the trick
(as in Aqre) is to start from a partition drawn along the answer's
rectangle boundaries — every region all-or-nothing, quota alone finishes
— and then thin numbers at the target level. That mass-produces quota,
corner and box grades at every size.
What's hard to fish is the top. A thinned board that stalls under box but
falls to probe shows up in 1–2% of attempts; at 10×10 the run found 3
in 10,000 attempts (at attempts 2,041 / 6,149 / 8,553). Nurimisaki lost
its bottom grades, Aqre lost its middle; Chocona thins out only at the
top — when two equivalent propagators cover for each other, the gap
"unique but not propagation-solvable" itself becomes rare. The UI greys
out what the bank lacks.
Shipped boards prove uniqueness with a median of 0 search guesses at
every size — the fixpoint alone completes the proof.
Probe = uniqueness, restored
This series keeps score on one law: a board with a unique solution
should fall to the probe fixpoint. It broke in Kurotto, held in
Nurimisaki, broke again in Aqre. In Chocona it holds on every unique
board found — 69 of them (4 from the section-1 pools, plus a
400-board-per-size maxSize-2 stream: 0/52 resist at 6×6, 0/13 at 8×8).
Two breaks, two restorations. The scoreboard carries to the next puzzle.
Verification
- Solution-count cross-check: a brute force that shares no code with the rule ladder — row-major DFS pruned only by region tallies and bounding boxes, every leaf scored by a standalone validator — agrees with the propagating search at all four levels on every (board, level) pair both can finish: 536/536, with 24 weak-level searches reported as capped rather than silently shaped. The ladder reasons only through 2×2 windows and the brute force prunes only with boxes, so the agreement is a machine check of the local⟺global equivalence.
- Exhaustive anchors: the clue-free 2×2, 3×3 and 4×4 boards are enumerated by a third engine built on the pairwise-bounding-box formulation — 12 / 208 / 10,148 boards, matching both other engines.
- Bank integrity: all 58 shipped boards re-checked unique by the searching engine, graded by the weakest level that finishes them without guessing.
42 tests. npm test runs them all.
Takeaways
- Chocona's rectangle law equals a local test — no 2×2 with exactly three shaded — and the puzzle's signature move is the inversion: three in a square force the fourth shaded.
- Split one theorem across three engines (definition, local double, pairwise-box) and their 536/536 agreement machine-checks it.
- Ablation: equivalent formulations are interchangeable propagators; only the number-reading quota rule is irreplaceable.
- The configuration space is huge (10,148 boards at clue-free 4×4), so raw streams carry almost nothing; the setter's dial is a cliff, the density dial is dead, and a third dial — the answer's own rectangle scale — is what moves uniqueness.
- Generation is search-free dart-throwing in O(n²); Aqre's eight-hour hang is structurally impossible.
- Probe = uniqueness holds, 69/69. Series score: two breaks, two restorations.
TypeScript + Vite, no runtime dependencies. All code is public.
Top comments (0)