Solving Heyawake: compiling the one rule that crosses rooms into clauses

Heyawake in the browser with three rule sets inside. The grid is cut
into rectangular rooms. Shade cells so no two shaded cells touch, the
unshaded cells stay one connected region, a numbered room holds exactly that
many shaded cells — and no straight run of unshaded cells passes through
three rooms. That fifth rule is the odd one out: its subject is a maximal
white run, which is redrawn on every move, and it is the only rule that
ties two rooms together. It compiles — from the room geometry alone, before
a single cell is decided — into a fixed set of at-least-one-shaded clauses.
Then the measurements get interesting. Puzzle #25 in the solver-included
series.

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

The rules

1. The grid is partitioned into rectangular rooms.
2. Shade cells. No two shaded cells touch orthogonally.
3. The unshaded cells form one connected region.
4. A numbered room holds exactly that many shaded cells.
5. No straight run of unshaded cells passes through three or more rooms.

Four small rules and one strange one

rule	subject
no two shaded cells touch	a pair of adjacent cells
a numbered room holds n shaded cells	one room
the unshaded cells are connected	the board, but it is the standard flood
no white run crosses three rooms	a maximal run, redrawn on every move

Rule 5 is unlike the others in two ways.

Its subject moves. A "maximal run of unshaded cells" can stretch the whole
width of the board, and shading a single cell snaps it into two different runs.
The thing the rule quantifies over is re-derived after every move.

It is the only rule that couples two rooms. Take it out and rooms speak to
each other solely through the no-touching rule at a shared border. Numbers stay
inside their own room. Rule 5 is what carries a fact about room A over to room C.

Compiling it away

The move is simple:

If a window of consecutive cells in a line touches three rooms, it cannot
be all-white. So at least one cell in the window is shaded.

That is an ordinary at-least-one clause. The only question is which windows to
enumerate.

This is where rooms being rectangles pays. A rectangle meets a line in
exactly one contiguous interval, so reading a row left to right gives a clean
sequence of room segments. The minimal three-room windows are therefore easy
to name: the last cell of segment i, all of segment i+1, and the first cell of
segment i+2.

for (let i = 0; i + 2 < segs.length; i++) {
  out.push({
    cells: [segs[i][segs[i].length - 1], ...segs[i + 1], segs[i + 2][0]],
    line,
    index,
  });
}

Every larger three-room window contains one of these, so the minimal list says
everything the rule says. And it depends only on the room layout — not on the
board state — so it is built once, before a single cell is decided.

The clause count is a closed form over the geometry: the sum over the 2n lines
of max(0, segments − 2).

size	rooms	span clauses	avg clause length	longest
5×5	6.9	7.8	3.3	5
7×7	11.7	23.6	3.5	7
9×9	20.9	49.8	3.6	8

Average length 3.5 — a minimal window is len(segment i+1) + 2 cells, so thin
rooms give short clauses.

Once it is a clause list, GAC on it is plain unit propagation: a clause with
every cell white is dead, a clause with one cell left forces it shaded. The
exotic rule has become an ordinary CSP part.

How do you know the compilation is right?

Get one window wrong and the solver lies quietly. So the validator is written
independently and never looks at a clause. It walks every maximal white run
and counts the distinct rooms it touches:

for (const line of ['row', 'col'] as const) {
  for (let index = 0; index < n; index++) {
    let seen = new Set<number>();
    for (const k of lineCells(n, line, index)) {
      if (state[k] === SHADED) seen = new Set();
      else {
        seen.add(puzzle.roomOf[k]);
        if (seen.size >= 3) return false;
      }
    }
  }
}

A 900-board property test then asserts every clause satisfied ⇔ the run scan
passes. Zero disagreements. If that ever splits, it is a compilation bug.

The three rule sets

local — no-touching, room numbers, connectivity. Heyawake as seen by a
player who forgot rule 5. Shipped as the falsified rival.

spans — the same, plus unit propagation on the compiled clauses, all
driven to a joint fixpoint.

probe — singleton consistency: assume a cell shaded, run spans to
fixpoint, erase it if the board dies, and the other way round.

Reach, measured over unique boards generated with no solvability filter (with
one, the last column would be circular):

size	local	spans	probe
4×4	0%	30%	100%
5×5	0%	13%	93%
6×6	0%	3%	82%
7×7	0%	0%	63%
8×8	0%	0%	49%

Zero at every size. Not "weaker" — the local rules finish nothing.

The 900-position property test says it from the other side:

the local set saw a cell the span set missed ......   0 / 900   (subsumed)
the span set saw a cell the local set missed ...... 846 / 900   (94%)
average advantage over all 900 positions .......... +11.3 cells

The 0 is structural, not luck: spans runs every rule local runs, so
containment holds by construction and the test just pins it. The interesting
side is the other one — a gap in 94% of positions, 11.3 cells on average.
For comparison, in the previous puzzle in this series (Tapa) the winning rule
was ahead in 65% of positions at +5.7 cells. This one is far more lopsided.

A sharper question: what actually pins the solution down?

Propagation strength is one measurement. Here is another.

Take the shipped 5×5 boards, switch the span rule off in the validator, and
count solutions again. Numbers, no-touching and connectivity all stay.

boards ................................... 60 (5x5, all unique)
still unique without the span rule .......  1 (2%)
median solutions without it .............. 978
mean ..................................... 1843
worst .................................... 12915

59 of 60 stop being unique. Median 978 solutions, worst 12,915.

So the numbers printed on the board are not the main thing narrowing the answer
down. The way the rooms are cut is. Heyawake wears the costume of a counting
puzzle; underneath it is closer to a geometry puzzle.

The same geometry cuts the other way too: 10–13% of random room layouts admit
no legal shading at all. The windows demand more shaded cells than the
no-touching rule can supply. The generator finds out by asking a complete solver,
and rerolls.

Two things worth stealing

"It finished" is a uniqueness certificate

Every propagator here is sound: a cell it fixes has that value in every
solution. Therefore:

If a rule set decides the whole board and the result survives the independent
validator, there cannot be a second solution.

So the generator never runs a search per removed clue. One call does uniqueness
and difficulty at the same time:

export function finishes(puzzle: Puzzle, ruleset: RuleSet): boolean {
  const state = makeState(puzzle);
  return propagators[ruleset](state, puzzle) && !state.includes(UNKNOWN) && isValid(state, puzzle);
}

Connectivity in one pass, not cells²

"A cell whose shading would split the white region must stay white" is usually
written by removing each cell in turn and re-flooding — O(cells²). Replace it
with a single Tarjan articulation walk: a DFS child c of u is severed when
low[c] >= disc[u], and u is forced white as soon as a severed subtree holds a
white cell while another white cell sits outside it.

Both versions ship — cutCells and cutCellsNaive — and a 600-state property
test demands they agree cell for cell. Together with a cheaper fixpoint test
(count of decided cells instead of hashing the board) it took 8×8 generation from
about 9s to about 1.9s per board.

Soundness: four counters must agree

Series standard. An independent brute force that shares no code with the
propagators enumerates every shading — pruning only on incremental adjacency —
and hands each leaf to isValid. Solution counts are then produced four ways:
brute force, local search, spans search, probe search.

A disagreement means one of them dropped or invented a solution, and that is how
an unsound rule — or a wrong window — gets caught. 103 tests.

The difficulty knob finally means something

In earlier puzzles of this series, probing finished every generated board, so the
only real difficulty knob was size.

Not here. Probing finishes 63% of 7×7 boards and 49% of 8×8 boards. Boards that
genuinely need search are common.

So the generator carves clues away against the rule set you pick. Choose
"spans only" and you get a board that really is solvable with the clauses, the
numbers and connectivity alone. The Level control is a knob, not a label.

Takeaways

• Heyawake's fifth rule quantifies over maximal white runs and is the only rule that ties two rooms together.
• Rooms are rectangles, so a line meets each room in exactly one interval. That names the minimal three-room windows — last of segment i, all of i+1, first of i+2 — and turns a non-local rule into a finite clause set built before the board exists.
• The clause count is a closed form: sum over the 2n lines of max(0, segments − 2). About 50 clauses at 9×9, average length 3.6.
• Without those clauses the local rule set finishes 0% of boards at every size; over 900 positions spans was ahead in 846 of them, +11.3 cells.
• Sharper still: switch the span rule off in the validator and only 1 of 60 unique boards stays unique, median 978 solutions. The geometry pins the answer down, not the numbers.
• The same geometry over-constrains: 10–13% of random layouts have no legal shading at all.
• With sound propagators, "it finished" is a uniqueness proof — the generator skips search entirely because of it.
• Soundness is pinned by four counters, including an independent brute force, that must agree on solution counts. 103 tests.

Which puzzle should fall next?

---

SEN LLC — software development and technical consulting
🌐 https://sen.ltd