Solving Futoshiki with bounds propagation: one-edge rules, chain-length conclusions

Futoshiki (不等号 / "inequality") in the browser with a
bounds-propagation solver inside. Fill an n×n grid so every row and
column holds each value 1..n exactly once while every < / >
sign between neighbouring cells tells the truth. Unlike the shading
puzzles earlier in this series, the unknown is a value in 1..n, so a
cell is a candidate bitmask and the rules shrink sets: duplicate
eviction, hidden singles, and — the star — a bounds rule that clamps
one floor and one ceiling per sign. That rule only ever looks at one
edge, yet run to a fixpoint it performs interval arithmetic over whole
inequality chains: the cell k steps up a chain ends up with floor k+1, a
global, chain-length conclusion no single rule ever computed. Solver-backed
puzzle #15.

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

The rules, and a change of model

A Futoshiki board is n×n. A finished board satisfies:

1. Every row and every column holds each of 1..n exactly once (a Latin square).
2. Every sign between two orthogonally adjacent cells is true (a < b means a really is smaller).

Clues come in two kinds — a few given digits, and the inequality
signs in the gutters. Most of the bundled boards are signs only.

The shading puzzles before this one (Nurikabe, LITS, Hitori…) had a one-bit
unknown per cell, so a three-valued cell was enough. Futoshiki's unknown is a
value, so each cell becomes a candidate set, stored as a bitmask in
one integer:

export function fullMask(n: number): number {
  return (1 << n) - 1;          // all of 1..n possible
}
export function minVal(mask: number): number {
  return 32 - Math.clz32(mask & -mask);   // smallest candidate = floor
}
export function maxVal(mask: number): number {
  return 32 - Math.clz32(mask);           // largest candidate = ceiling
}

The point of the encoding: minVal / maxVal read directly as the ends of
an interval.

Three propagation rules

Duplicate — a solved cell evicts its value from its row and column; an
emptied mask is a contradiction:

const bit = 1 << (v - 1);
for (const m of g.peers[i]) {
  if (state[m] & bit) {
    state[m] &= ~bit;
    if (state[m] === 0) return false;
  }
}

Hidden single — if a value has exactly one home left in a line, it moves
in; zero homes is a contradiction.

Bounds — a sign a < b translates into two clamps: a may only keep
values below b's current ceiling, and b only values above a's
current floor:

for (const { lo, hi } of p.ineqs) {
  const clampedLo = state[lo] & below(maxVal(state[hi]));      // lo < max(hi)
  const clampedHi = state[hi] & above(minVal(state[lo]), g.n); // hi > min(lo)
  ...
}

All three run to a fixpoint. No guessing.

The show: one edge per step, whole chains per fixpoint

Each application of the bounds rule looks at one edge. Iterated to a
fixpoint, something bigger emerges: interval arithmetic over the whole
inequality graph.

Take a < b < c < d across a 4×4 row. Pass one: a < b lifts b's floor to
2, b < c lifts c's to 3, c < d lifts d's to 4 — while the ceilings
tighten the other way and a drops to 1. In general the cell k steps from
the bottom of a chain gets floor k+1, and k steps from the top gets ceiling
n−k. A chain of n−1 signs pins all n cells outright, and the test suite
states exactly that:

it('derives chain-length floors from pairwise clamps alone', () => {
  // a < b < c < d: every rule step saw one sign,
  // yet the fixpoint pins the whole row to 1234.
  const p = puz(['....', '....', '....', '....'], [
    { lo: 0, hi: 1 }, { lo: 1, hi: 2 }, { lo: 2, hi: 3 },
  ]);
  const s = initialState(p);
  expect(propagate(s, geom(4), p)).toBe(true);
  expect([0, 1, 2, 3].map((i) => solvedVal(s[i]))).toEqual([1, 2, 3, 4]);
});

In constraint-programming terms this is bounds consistency enforced
edge-by-edge rather than full arc consistency: it never looks at holes in the
middle of a candidate set, but inequality is an order constraint, so floors
and ceilings carry all the strength you need. Cheap local clamps, run to a
fixpoint, flood bounds across chains, forks and joins of the sign DAG.

Contradiction detection falls out of the same machinery for free — put four
< signs in a 4-value board and some floor demands a 5, emptying a mask:

it('contradicts a chain longer than the board allows', () => {
  // 4 strict increases need 5 distinct values — impossible in a 4×4.
  expect(propagate(initialState(p), geom(4), p)).toBe(false);
});

Search and the uniqueness proof

When propagation stalls, the solver branches on the fewest-candidates
cell, tries values in ascending order, and re-propagates. solveAll(p, 2) is
a complete enumeration that stops at two solutions, so length === 1 is a
proof of uniqueness.

Boards are authored by deletion

The generator (tools/generate.mts) works answer-first. Build a random Latin
square by backtracking, read the true sign off every adjacent pair — all
2n(n−1) of them — at which point the board is trivially unique. Then
greedily delete clues in random order, keeping a deletion only while the
engine still proves exactly one solution. Givens go first, so the boards end
up sign-driven (two of the six have no givens at all).

What survives is a locally minimal clue set: removing any single
remaining clue breaks uniqueness. The test suite checks that claim on every
board:

it('is minimal: dropping any one sign breaks uniqueness', () => {
  const dropped: Puzzle = { n, givens, ineqs: ineqs.slice(1) };
  expect(hasUniqueSolution(dropped)).toBe(false);
});

Not just "this board is unique" but "every remaining sign is
load-bearing." 55 tests in all.

Takeaways

Futoshiki is this series' first multi-valued domain — cells became
candidate bitmasks and propagation became set-shrinking. The star is the
bounds rule: a cheap clamp that sees one edge at a time, yet whose fixpoint
performs interval arithmetic across entire inequality chains, producing
global, chain-length conclusions (floor k+1 at height k) that no single rule
ever computed. Duplicate eviction and hidden singles cover the Latin side; a
fewest-candidates search proves uniqueness; and the bundled boards are thinned
from the full sign set until every surviving clue carries weight.
Solver-backed puzzle #15.