DEV Community

SEN LLC
SEN LLC

Posted on

Solving Binairo with a line dictionary: every human trick is one projection

#typescript #algorithms #gamedev #puzzle

Binairo (Takuzu, binary puzzle) in the browser with a
line-dictionary solver inside. Three rules: no three equal circles
in a line, every row and column half black / half white, and no two
rows (or columns) alike. The solver implements none of the human trick
catalog. Instead it enumerates — once per size — the dictionary of
balanced, triple-free binary words, treats each row and column as a
variable over that dictionary, and projects: a cell on which every
surviving candidate word agrees is decided. Sandwiches, pairs and
counting arguments all fall out as shadows of that single projection,
and the no-duplicate rule becomes alldifferent over the dictionary.
Solver-backed puzzle #19.

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

Screenshot

The rules: three of them, one global

A finished n×n board (n even) satisfies:

  1. no three consecutive equal cells in any row or column;
  2. every row and column holds exactly n/2 of each color;
  3. no two rows are identical — and no two columns.

Rules 1 and 2 are local to a line. Rule 3 crosses lines, and human
technique lists treat it as its own special move ("don't copy that
finished row"). In the solver it melts into something standard.

The dictionary: every legal line, enumerated once

Restricted to a single line, rules 1+2 describe the set of n-bit words
with exactly n/2 set bits and no run of three:

export function lineWords(n: number): number[] {
  const words: number[] = [];
  for (let w = 0; w < 1 << n; w++) {
    if (popcount(w) === n / 2 && !hasTriple(w, n)) words.push(w);
  }
  return words;
}
Enter fullscreen mode Exit fullscreen mode

The counts are tiny: 14 words at n=6, 34 at 8, 84 at 10, 208 at 12 —
the central binomial coefficient minus the words with a triple. Even on a
10×10 board a row has only 84 possible shapes. That is the whole trick of
this build: each row and column becomes one variable over a small
dictionary, not a string of cells.

Propagation = filter + project

For each line, keep the dictionary words matching its decided cells, then
AND and OR them together:

const cands = candidates(grid, size, isRow, idx);
if (cands.length === 0) return false; // contradiction
let and = full, or = 0;
for (const w of cands) { and &= w; or |= w; }
// open cell with the AND bit set   → decided BLACK
// open cell with the OR bit clear  → decided WHITE
Enter fullscreen mode Exit fullscreen mode

A cell on which every surviving word agrees is decided. Run that to a
fixpoint and the entire human catalog appears as its shadow:

  • sandwich 1 _ 1 → the middle is 0, because a 1 there would be a triple, so no candidate has it;
  • pair 1 1 → both flanks are 0, same reason;
  • counting — a color at quota flips the rest of its line, because unbalanced words aren't in the dictionary.

None of these is implemented anywhere. One filter subsumes them all, and
per line it is exactly as strong as full enumeration — the same skeleton
as nonogram line solving.

Rule 3 is alldifferent over the dictionary

A word already spent by a finished parallel line is removed from every
sibling's candidates:

for (const w of lineWords(size)) {
  if ((w & mask) === val && !spent.has(w)) out.push(w);
}
Enter fullscreen mode Exit fullscreen mode

That one !spent.has(w) generalizes "don't copy the finished row" and
buys two things. A row two cells short of copying a finished twin gets
forced into the swap (the copy is filtered out, one candidate
remains). And if two identical finished lines ever do appear, each wipes
out the other's only candidate — duplicates surface as a plain empty
domain, no separate check needed.

Search and the uniqueness proof

When the fixpoint stalls, branch on the line with the fewest
candidates. After a fixpoint an undecided line always has at least two
(a single candidate would have been projected onto every cell), so every
branch is a genuine choice point. Counting solutions with a cutoff at two
proves each of the six bundled boards (6×6 … 12×12) has exactly one
solution.

Boards are authored answer-first: build a full grid row-by-row out of the
dictionary — keeping every column prefix legal makes column balance free —
then greedily delete givens while uniqueness survives. The test suite
checks every surviving given is load-bearing: drop any one and the
solver finds a second solution. A 6×6 board gets down to 7 givens out
of 36.

Takeaways

  • Lift the domain from cells to lines and a zoo of local tricks collapses into one projection. Building the ground the tricks grow from beats implementing the tricks.
  • The global no-duplicate rule, once lifted, is just alldifferent — a shape constraint solvers have known forever.
  • 39 tests, TypeScript, zero runtime dependencies, engine ≈ 230 lines.

All the code is public: https://github.com/sen-ltd/binairo

Top comments (0)