Solving Thermometers: the enumeration rule that won Kakurasu provably collapses into interval arithmetic

Thermometers in the browser with two sound rule sets inside.
Mercury fills every thermometer from the bulb, contiguously; row and
column clues count the filled cells. A thermometer is one scalar
variable — how far the mercury reaches — and that monotonicity comes
with a small theorem: per-line witness enumeration, the rule that
beat interval arithmetic in the previous puzzle of this series,
provably does nothing here. A property test agrees: 900 positions,
zero disagreements. The machine strength has to come from somewhere
else — probing: assume a level, propagate, erase the levels that
die. Measured: intervals alone finish 86% of unique 8×8 boards; probing
finished 600 of 600. Puzzle #23 in the solver-included series.

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

Pick the right variable

The rules fit in two lines. The grid is partitioned into path-shaped
thermometers; mercury pours from the bulb without gaps; each row and
column clue counts that line's filled cells.

The naive model is a boolean per cell, with contiguity checked as a
constraint. The right model folds contiguity into the variable itself:

f_t ∈ {0, 1, ..., len(t)}   — how far thermometer t's mercury reaches
cell (t, p) is mercury  ⟺  p < f_t     (p = distance from the bulb)

One scalar per thermometer, and every line becomes a sum of that line's
crossings' contributions.

One geometric trap: thermometers snake, so one can cross the same row
twice — in ~11% of multi-cell crossings the cells are not even
adjacent in the line, and 99% of 8×8 boards contain such a crossing. The
filled cells in a line are not a contiguous segment. They are, however,
always a prefix in thermometer order — and every argument below runs
on that order, not on line geometry.

The human rule set: interval arithmetic

Keep each level as a range [lo, hi]. Both user marks only clamp it
(mercury raises lo, a cross lowers hi). Per line, the same interval
reasoning as Kakurasu:

needMin(t) = clue − Σ_{s≠t} cmax(s)   — what the others can't cover
needMax(t) = clue − Σ_{s≠t} cmin(s)   — what the others already force
→ clamp t's contribution count into [needMin, needMax]
→ the count is monotone in f_t, so [lo, hi] tightens directly

Run all lines to a fixpoint. Cells under every surviving level are
mercury; cells over all of them are air.

The machine rule set (that was supposed to be)

Kakurasu, one puzzle ago in this series, was won by per-line witness
enumeration: list every subset of weights that meets the clue, keep
only what all witnesses support. With witnesses {2,4} and {1,2,3}, the
2 is forced — while interval arithmetic stays silent in both directions.
Per-line GAC, strictly stronger than intervals.

I ported that rule to Thermometers, wrote the comparison test, ran it —
and the two propagators agreed everywhere. 900 positions, zero
disagreements. I went hunting for the bug and found a five-line proof
instead:

a mercury level moves in unit steps
→ its contribution count to a line changes by 0 or 1 per step
→ over an interval domain, the count sweeps a gap-free range
→ the sums the other crossings can contribute form an interval
→ "some witness completes the clue" ⟺ "the count fits an interval"

So per-line enumeration lands exactly on the interval fixpoint — and
from every reachable position, because user marks only ever clamp levels
from both ends: domains stay intervals, and no holes ever appear for
enumeration to exploit.

The difference from Kakurasu is the type of the line variable. There it
was a subset of weights, and witness sums could be gappy. Here it is
a water level. Monotonicity flattens enumeration. The defeated rule
stays in the codebase (propagateLineGAC) as a falsified rival, with the
equality pinned by a property test.

The machine rule set that actually exists: probing

So what solves the boards where intervals stall (14% at 8×8)? If
enumeration inside a line is worthless, strength can only come from
across lines:

for each thermometer t, each candidate level f:
  assume f → run intervals to fixpoint → contradiction? erase f
iterate until nothing dies

Singleton consistency over intervals: it converts "this level overflows a
line three inferences away" into a one-step erasure. The Hint button
names whichever rule fires: bookkeeping (mercury below mercury, air above
a cross), one line's count, chained counts, or a probe.

The measurements

200 boards per size per experiment; reproduce with
npx vite-node tools/stats.mts.

1. Uniqueness is bought by rejection. Random levels over a random
partition are unique:

size	unique on the first roll
4×4	94%
6×6	57%
8×8	8%

The generator just rerolls levels — 19 rerolls per accepted 8×8 board,
~10 ms each.

2. Rule-set reach on unique boards:

size	intervals finish	probing finishes
4×4	100%	100%
6×6	98%	100%
8×8	86%	100%

Probing solved every unique board sampled, so every shipped board is
guess-free and the Hint button never runs dry. The failure shape is the
interesting part: when intervals stall at 8×8, they stall 26.3 of 64
cells in — mid-game. The exact opposite temperament of Suguru's singles
two puzzles ago, which died 3.7 cells into the opening.

3. The size dial is the difficulty dial, again. Boards needing a
probe: 0% at 4×4, 5% at 6×6, 19% at 8×8.

Soundness: four counters that must agree

Series standard equipment. An independent brute force over mercury levels
(sharing no code with the propagators) sits next to propagation-backed
search under intervals, enumeration, and probing — four solution
counters, and the tests demand full agreement on random boards of every
size. An unsound rule gets caught here, as a count mismatch. Hand-built
fixtures cover a unique board, a zero-solution board, a two-solution
board, and a board that intervals cannot finish but probing can. 59 tests
total.

Takeaways

• Model the thermometer as a scalar — the mercury level. Contiguity folds into the variable and disappears.
• The enumeration rule that won Kakurasu is provably identical to interval arithmetic here. Enumeration only wins when domains can have holes; a water level cannot.
• Real machine strength came from probing across lines: 86% → 600/600.
• Soundness is pinned by four solution counters in full agreement, brute force included.

Next puzzle to flatten is loading.

---

SEN LLC — Software development & technical consulting
🌐 https://sen.ltd