DEV Community

SEN LLC
SEN LLC

Posted on

Solving LITS: the puzzle whose name is a theorem, and uniqueness means killing tetromino slides

LITS in the browser with three rule sets inside. The grid is cut into
regions; shade exactly four cells in every region, forming a
tetromino; all shaded cells form one connected mass; no 2×2
square
is fully shaded; and where two tetrominoes from different regions
touch, they must not be congruent (rotations and reflections count as
the same shape). The puzzle is named after the allowed tetrominoes — L, I,
T, S — with the fifth, O, forbidden. But O is the 2×2 square, and the 2×2
square is already illegal. The constraint in the name is a theorem.
Puzzle #27 in the solver-included series.

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

Screenshot

The rules

  1. The grid is cut into regions (polyominoes of four or more cells)
  2. Every region holds exactly four shaded cells forming a tetromino
  3. All shaded cells form one orthogonally connected mass
  4. No 2×2 square is ever fully shaded
  5. Touching tetrominoes from different regions must not be congruent

The allowed tetrominoes are L, I, T and S. The O — the square — is forbidden.
That last clause is where this build starts.

The name is redundant

There are five tetrominoes: L, I, T, S, O. The name LITS declares four of them
legal, excluding only O. But O is the unique tetromino that is a 2×2 square,
and rule 4 already outlaws a fully shaded 2×2 square.

So the "L, I, T, S only" clause is redundant. Weaken rule 2 to "four
connected cells", never mention a shape name, and the puzzle does not change
at all.

That is not just an argument — it is an exhaustive test. A 5×5 board has
228 connected 4-subsets; exactly 16 of them contain a
2×2 square, and those are precisely the ones the shape classifier calls O:

it('THE THEOREM: for connected 4-sets, being O is exactly containing a 2×2 square', () => {
  // enumerate every 4-subset of a 5×5 board and check
  // "contains a square" ⟺ "classifies as O", one by one
  expect(hasSquare).toBe(shape === 'O');
});
Enter fullscreen mode Exit fullscreen mode

So the engine holds no list of allowed shapes anywhere. shapeOf is a
connectivity check plus a case split on the bounding box — a connected 4-cell
set can only span 1×4, 2×2 or 2×3 boxes, because a 4-cell path spreads at most
(rows−1)+(cols−1) = 3 steps — and O dies as a shadow of the square rule.

The region is the variable, again

Like Norinori before it, nothing is written on a
LITS board. The partition is the puzzle, so the natural variable is not the
cell but the region. In Norinori a region's decision was "which two cells";
its domain was C(k,2) pairs. Here the decision is "which tetromino, where",
and the domain is the region's list of placements — its connected non-O
4-subsets, a handful to a few dozen per region.

The lifting's payoff is that the puzzle's signature rule dissolves. "Congruent
shapes must not stare at each other across a border" — a statement about
equivalence classes of shapes — becomes an ordinary binary constraint between
adjacent regions:

export function binaryOk(state, puzzle, i, pi, j, pj): boolean {
  // touching with equal shapes: incompatible
  if (pi.shape === pj.shape && placementsTouch(pi, pj, n)) return false;
  // a 2×2 square closing across the border: incompatible
  for (const s of sharedSquares(i, j)) {
    if (squareCells(s, n).every((k) => read(k) === SHADED)) return false;
  }
  return true;
}
Enter fullscreen mode Exit fullscreen mode

Enforcing it is textbook AC-3. Cells every surviving placement shades are
shaded; cells none touches are white.

Connectivity refuses to decompose

"One connected mass" is a property of the whole board; no amount of squinting
turns it into a constraint between two regions. So it gets its own global
propagator
:

  • a cell is possibly shaded when some surviving placement of its region covers it;
  • every placement, being connected, lives inside exactly one component of the possibly-shaded graph;
  • a solution's shaded mass is connected and meets every region — so it can only live in a component that still offers every region a placement;
  • placements in any other component are stranded, and get pruned.
// only components that still offer every region a placement are viable
const viable = components.filter((c) =>
  regions.every((i) => live[i].some((p) => componentOf(p) === c)),
);
// prune stranded placements, then loop with AC-3 to a joint fixpoint
Enter fullscreen mode Exit fullscreen mode

Three rule sets

  • local — count each region to four, close any three-quarter 2×2 with a white cell, repeat. The puzzle as seen by a solver that never leaves the cell. It sees no shapes and no connectivity, and ships as the falsified rival.
  • tetro — the local rules plus AC-3 on the placement domains plus the connectivity propagator, to a joint fixpoint.
  • probe — singleton consistency on top: assume a cell, propagate, watch the board die.

A rule set that finishes a board with no search is a uniqueness
certificate
: every propagator is sound — each cell it fixes has that value in
every solution — so a completed board that passes the independent validator
cannot have a second solution.

Completion rates, measured on unique boards generated with no solvability
filter (a lesson from earlier in this series: filtering by solvability and
then reporting solvability is circular):

size local tetro probe mean region
6×6 0% 85% 100% 6.0
8×8 0% 60% 100% 6.4

A 900-position property test says the same thing from the other side: the
lifting decided more cells than the local rules in 896 of 900
positions, +13.8 cells on average, and the local rules never once won.

Generation: density is destiny

The only thing a LITS generator can vary is the partition — and a random
partition is essentially never a puzzle. Norinori failed that way too, but in
the opposite direction: its random partitions mostly had no solution.
LITS random partitions (region sizes 6–10):

size none exactly one two or more
6×6 7% 0% 93%
8×8 12% 0% 88%

Exactly-one never happened. Nearly everything dies on the "far too many"
side.

The culprit is arithmetic. Every region shades exactly four cells, so mean
region size = 4 / shaded fraction
, an identity. At 45% shading regions
average nine cells, each dragging a C(9,4)-sized placement domain, and the
board is hopelessly loose. Tight boards demand high density and small
regions
— and greedy tetromino accretion jams around 55% shading, because
the square rule and the congruence rule bind together at density. Randomised
backtracking packing — shuffle candidates, try twelve, undo on dead ends —
reaches 65%: regions of six and a half cells.

One more greedy choice matters: each unshaded cell floods into whichever
neighbouring region it enlarges the least, measured in placements. That
alone cuts the raw partition's solution count by orders of magnitude: the
smallest-region flood pins the counter against its 3000 cap, while the
domain-greedy flood lands at a median of 36 (min 6, max 747).

The last rivals standing are slides

Autopsy a nearly-unique board — enumerate its full solution set — and the
rivals always look the same:

sol0: differs at [5,39]     ← regions 0 and 2
sol1: differs at [5]        ← region 0 alone
sol2: differs at [5,29,39]  ← regions 0, 3, 2
...
(8 solutions = the 2³ lattice of 3 independent slides)
Enter fullscreen mode Exit fullscreen mode

Ambiguity, at the end, is a tetromino sliding or pivoting inside a single
region
while everything else stays put — and stuck boards carry a whole
lattice of independent slides.

So define a region's local slack: the number of other tetrominoes it
could hold with every other region's shading left exactly as the intended
solution has it. Total slack 0 kills every single-region rival, and — this is
the point — slack is computable per region, incrementally, without ever
counting solutions
: list the placements, run each through the independent
validator.

The generator's endgame is slack descent. The only move is migrating a cell
the solution leaves white into a neighbouring region — a move that can
never hurt the intended solution, because no shaded cell changes region, so
every region keeps its exact tetromino and the global rules see nothing move:

  1. shrink total placement-domain size (incremental, stateless, fast);
  2. descend total slack to zero; when no single move improves, peel a white cell off a slacky region — a smaller region has fewer placements and nowhere left to slide;
  3. slack cannot see rival solutions that rearrange several regions at once, so a final full search confirms, rejecting the rare board that still has one.

The counterexample-walking that generated Norinori — find a rival, kill it
with one move, repeat — does not work here: from thousands of rivals,
one-kill-per-step never converges, and the cells to kill end up buried in
region interiors with no legal move. Descending the structure (slack)
instead of the count is what cracked it.

Three rules, unequally load-bearing

Take the shipped 6×6 boards and switch one rule off in the validator:

dropped rule boards still unique median count
congruence (touching twins allowed) 1/16 4
connectivity 12/16 1
the 2×2 square (which also re-admits O) 0/16 159

Congruence and the square rule each carry almost the whole bank: drop either
and 15 or all 16 boards stop being unique. Connectivity is the odd one out —
12 of 16 stay unique without it, so it decides only 4 boards. But on those
4 it is the only thing holding uniqueness up. No rule is decoration; the load
is just nowhere near evenly spread. And the shipped banks' letter demographics:
6×6 (96 regions) L=29% I=28% T=22% S=21%, with 2 of 16 boards missing a letter; 8×8 (160 regions) L=32% I=27% T=22% S=19% and 10×10 (240 regions) L=31% I=22% T=22% S=25%, neither missing a letter anywhere. The share of adjacent region pairs whose tetrominoes actually touch falls as boards grow: 72% → 61% → 57%.

Soundness is four counters agreeing

Two brute-force counters share no code with the propagators — one walks the
cells in row-major order with incremental pruning, one walks the regions
choosing placements — plus a propagation-backed counter per rule set, plus an
independent validator that re-derives every shape from scratch. All of them
must agree on solution counts across randomly generated boards; a disagreement
is how an unsound propagator gets caught. 65 tests.

Takeaways

  • The four letters in LITS's name are a theorem, not a rule: the square rule already implies them. Verified exhaustively over all 228 connected 4-sets of a 5×5 board.
  • Lift the board to region variables with tetromino-placement domains: the congruence rule becomes textbook AC-3; connectivity needs its own global propagator built on component viability.
  • Random partitions were never once unique — the opposite failure mode to Norinori — because mean region size = 4 / density. Backtracking packing pushes density to 65% where uniqueness becomes reachable.
  • The last rivals are single-region tetromino slides; descend local slack — computable without counting solutions — and peel cells off slacky regions when stuck.
  • Soundness = four independent counters forced to agree; a propagation-only finish doubles as a uniqueness certificate.

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

Top comments (0)