DEV Community

SEN LLC
SEN LLC

Posted on

Solving Hitori with constraint propagation: the puzzle where propagation can't even start

Hitori (ひとりにしてくれ / "leave me alone") in the browser with a
constraint-propagation solver inside. Every cell carries a number; you
keep (white) or shade (black) each one so that kept numbers never
repeat in a row or column
, shaded cells never touch side-to-side, and
the kept cells stay one connected region. The unknown is the usual
one bit per cell, the model the usual three-valued cell — but on an untouched
board every dynamic rule is starved: the duplicate rule needs a white
cell to exist, the adjacency rule needs a black one, connectivity needs both.
Pure propagation is a no-op on move one. The only ways in are the
puzzle's two textbook openings — sandwich and pair — each a one-step
case analysis whose branches agree
, which is exactly the condition that
lets a case split masquerade as a sound propagation rule. Solver-backed
puzzle #14.

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

Screenshot

The rules, and the usual model

A Hitori grid is R×C with a number in every cell. A finished board keeps or
shades each cell so that:

  1. Among the kept cells, no number repeats in any row or column.
  2. Shaded cells are never orthogonally adjacent.
  3. The kept cells form one orthogonally-connected region.

Same unknown as Nurikabe — one bit per cell — so the model is the same
three-valued cell, shrunk by sound, guess-free implications only:

export const UNKNOWN = 0;
export const WHITE = 1;   // kept
export const BLACK = 2;   // shaded
Enter fullscreen mode Exit fullscreen mode

Three dynamic rules write themselves:

  • duplicate — a cell decided WHITE evicts every copy of its number from its row and column (two kept copies in one line is a contradiction).
  • adjacency — a cell decided BLACK whitens all four neighbours (two adjacent blacks is a contradiction).
  • cut cell — an UNKNOWN cell whose shading would disconnect the whites must itself be WHITE. No trial assignment needed: flood the non-black graph with that cell removed and see whether every white is still reached.

The trap: propagation has no seed

Here is where Hitori differs from every earlier puzzle in this series. A fresh
board is all UNKNOWN. The duplicate rule fires off an existing white, the
adjacency rule off an existing black, the connectivity check needs two whites —
so none of the three can fire on move one. Run them to a fixpoint and
nothing happens. In Nurikabe or Akari the printed clues pin cells from the
start; Hitori's clues (the numbers) directly decide no cell's colour.

The test suite states it outright:

it('is a clean no-op on a board with no pattern', () => {
  const p = puz(['12', '21']);
  const s = initialState(p);
  expect(propagate(s, geom(2, 2), p)).toBe(true);
  expect([...s]).toEqual([UNKNOWN, UNKNOWN, UNKNOWN, UNKNOWN]);
});
Enter fullscreen mode Exit fullscreen mode

The way in: case splits whose branches agree

Human solvers open every Hitori the same way, with two textbook patterns — and
implementing them is where the design clicks. Both are case analyses, yet
both are legitimate propagation rules, because every branch reaches the same
conclusion
.

Sandwicha ? a in one line. Shade the middle and both flanking as
survive as kept duplicates. So whichever a lives, the middle cell is
white
:

// sandwich: a ? a  =>  the middle cell is white.
for (let k = 1; k + 1 < line.length; k++) {
  if (p.values[line[k - 1]] === p.values[line[k + 1]]) {
    if (!assign(state, line[k], WHITE)) return false;
  }
}
Enter fullscreen mode Exit fullscreen mode

Pair — an adjacent a a. Not both kept (duplicate), not both shaded
(adjacent) — so exactly one survives. You don't know which, but you do know
the line now owns a kept a, so every other a in that line is black:

// pair: a a  =>  every other a in the line is black.
for (const m of line) {
  if (p.values[m] === v && !assign(state, m, BLACK)) return false;
}
Enter fullscreen mode Exit fullscreen mode

Both rules are static — their conclusions depend only on the printed numbers —
but they still run inside the fixpoint, because a "must be white" landing on an
already-black cell is a contradiction worth catching. The moment they inoculate
the board with its first blacks and whites, the dynamic rules cascade: a black
whitens its neighbours, a white evicts its twins, and the cut-cell rule rescues
whites about to be walled in.

An aside: Hitori never asks for a reason to shade

One rule subtlety only implementation made obvious: there is no minimality
constraint
. Nothing requires a shaded cell to deserve shading — any shading
that breaks no rule is a solution. A duplicate-free 2×2 board therefore has
five solutions (keep everything, or shade any single cell; the two diagonal
double-shadings die by disconnection):

const p = puz(['12', '21']);
expect(solveAll(p, 10).length).toBe(5);
Enter fullscreen mode Exit fullscreen mode

So a well-posed board must be unique the hard way: every gratuitous extra
shade has to die by adjacency or disconnection
. That lands squarely on the
generator.

Search, and the uniqueness proof

When propagation stalls, the search branches on the UNKNOWN cell with the
most decided neighbours, tries BLACK then WHITE, and re-propagates.
solveAll(p, 2) is a complete enumeration that stops at two solutions, so
length === 1 is a genuine uniqueness proof:

export function hasUniqueSolution(p: Puzzle): boolean {
  return solveAll(p, 2).length === 1;
}
Enter fullscreen mode Exit fullscreen mode

Boards are authored answer-first

The generator (tools/generate.mts) writes the solved shading before the
numbers. Scatter black cells (never adjacent, whites kept connected), then give
the white cells a shuffled Latin square's values — row/column uniqueness
among the whites holds by construction. Each black cell then copies a
value from a white cell in its own row or column
, so every shaded cell has a
visible reason: keep it and its line gains a duplicate. Finally the engine must
prove exactly one solution — which, per the aside above, includes proving
that every do-nothing extra shade dies. The tests re-check all of it per board:
the authored shading is legal, every black has its excuse, and the solver
recovers exactly the authored answer. 45 tests, 5×5 through 10×10.

Takeaways

Hitori hands you back the humble cell-bit unknown — and then starves the
propagator: no clue decides a cell, so sound dynamic rules alone cannot make
the first move
. The openings that unlock it are the puzzle's two classic
patterns, and the reason they're classic is structural: each is a one-step
case split whose branches agree
, the exact shape a case analysis must have to
count as propagation. Seed the board with them, let duplicate / adjacency /
cut-cell chain to a fixpoint, and a fewest-options search proves each bundled
board has exactly one answer. Solver-backed puzzle #14.

Top comments (0)