Heyawake

Four of the five rules are small. "No two shaded cells touch" is about a pair of cells. "This room holds three shaded cells" is about one room. Connectivity is global but standard. The fifth rule is the odd one: no straight run of unshaded cells may pass through three rooms. Its subject is a maximal white run, which can be as long as the board and which changes shape every time a cell is shaded — and it is the only rule in the puzzle that ties two rooms together.

You can compile it away. A window of consecutive cells that touches three rooms may not be all-white, so at least one of its cells is shaded — an ordinary clause. Rooms are rectangles, so a line meets each room in exactly one contiguous segment, which makes the minimal three-room windows easy to name: the last cell of one segment, all of the next, and the first cell of the one after. Every larger three-room window contains one of those, so this finite set says everything the rule says. It depends only on the room layout, so it is built once, before a single cell is decided:

Once it is a clause list, generalised arc consistency on it is just unit propagation, and the rule stops being exotic. What it does not stop being is load-bearing. Three rule sets ship here — local (adjacency, room numbers, connectivity — the puzzle as a player who forgot rule 5 sees it), spans (the same plus the clauses), and probe (singleton consistency on top). Measured over unique boards generated with no solvability filter, so the last column is not circular:

Zero, at every size. Not "weaker" — the local rules finish nothing at all. A 900-position property test says the same thing from the other side: the local set never decided a cell the span set missed (0 of 900, and it is provably subsumed), while the span set decided more in 846 of them.

And the rule carries the uniqueness too. Take the shipped 5×5 boards, switch the span rule off in the validator, and count again: only 1 of 60 stays unique, the median jumps to 978 solutions and the worst board to 12,915. The numbers on the board are not what pins the answer down; the geometry is.

The last row is the honest one: unlike the previous puzzles in this series, probing does not finish everything, so the shipped generator carves against the rule set you pick — the Level control is a real knob, not a label. Soundness is pinned by an independent brute-force solver that shares no code with the propagators and re-derives the span rule the slow way, by walking maximal white runs; four counters must agree on solution counts, and a disagreement is how a broken compilation gets caught. 103 tests.