バイナリーパズル（Binairo）を辞書で解く — 人間の定石は全部「1つの射影」の影

Binairo（Takuzu / バイナリーパズル） を、ライン辞書ソルバー内蔵でブラウザに実装した。ルールは 3 つ: 同色 3 連禁止・各行各列は白黒半々・同一の行（列）は 2 本禁止。ソルバーは人間の定石カタログ（サンドイッチ・ペア・数え上げ）を 1 つも実装しない。代わりにサイズごとに 1 回だけ、「1 本のラインとして合法な語」——均衡かつ 3 連なしの n ビット語の辞書——を列挙し、各行・各列をその辞書上の変数とみなす。伝播は各ラインの候補語を確定セルでフィルタし、射影する: 生き残った全候補が一致するセルは確定。定石は全部この 1 つの射影の影として勝手に出てくる。「同じ行を 2 本作らない」ルールは辞書上の alldifferent になる。ソルバー内蔵パズル第 19 弾。

🌐 ライブデモ: https://sen.ltd/portfolio/binairo/
📦 GitHub: https://github.com/sen-ltd/binairo

ルール: 3 つだけ、でも 1 つは大域的

完成盤（n×n、n は偶数）は次を満たす:

1. どの行・列にも同色の 3 連禁止
2. 各行・各列は白黒ちょうど半々
3. 同一の行は 2 本禁止。列も同様

1 と 2 はライン局所の制約だが、3 はライン同士を跨ぐ大域制約だ。人間向けの定石集では「完成した行のコピーを作らない」という別枠のテクニックとして扱われる。ソルバーではこれが一番きれいに溶ける。

辞書: 1 本のラインとして合法な語を全列挙

ルール 1 と 2 をラインだけで見ると、「n ビットで 1 がちょうど n/2 個、同じビットが 3 連続しない語」の集合になる。これはサイズごとに 1 回列挙してキャッシュできる:

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;
}

サイズは驚くほど小さい: n=6 で 14 語、8 で 34、10 で 84、12 でも 208。中央二項係数 C(n, n/2) から 3 連入りを引いた数だ。10×10 の盤でも「行の取りうる姿」は 84 通りしかない——ここが本作の肝で、各行・各列をセルの列ではなく辞書上の 1 変数として扱ってよいことになる。

伝播 = 候補フィルタ + 射影

各ラインについて、確定済みセルに合致する候補語を辞書から拾い、全候補の AND / OR を取る:

const cands = candidates(grid, size, isRow, idx);
if (cands.length === 0) return false; // 矛盾
let and = full, or = 0;
for (const w of cands) { and &= w; or |= w; }
// and にビットが立つ未確定セル → 黒で確定
// or にビットが立たない未確定セル → 白で確定

全候補が一致するセルは確定——これが射影で、伝播はこれを不動点まで回すだけ。人間の定石は全部この影になっている:

• サンドイッチ 1 _ 1 → 間は 0。中を 1 にする語は 3 連で辞書に無いから、全候補が 0 で一致する
• ペア 1 1 → 両脇は 0。同じ理由
• 数え上げ ある色がノルマ n/2 に達した → 残りは全部逆色。均衡でない語は辞書に無いから

どれも個別に実装していないのに、辞書フィルタ 1 個がライン単体の全列挙と同じ強さで全部を包含する。ノノグラムのライン走査と同じ構図だ。

ルール 3 は「辞書上の alldifferent」

完成した平行ラインが使った語は、他のラインの候補から取り除く:

// 行 idx の候補を拾うとき
for (const w of lineWords(size)) {
  if ((w & mask) === val && !spent.has(w)) out.push(w);
}

これは人間の「完成した行をコピーしない」の一般化で、副作用が 2 つある。まず、あと 2 マスの行が完成行と衝突する埋め方しか持たないとき、残る 1 通りに確定する（スワップ強制）。次に、同一ラインが 2 本できてしまった局面では、互いが互いの唯一の候補を潰し合って候補ゼロ = 矛盾として自然に検出される。重複チェックを別に書く必要がない。

探索と一意性証明

不動点で詰まったら、候補最少のラインで分岐する。不動点の後では未確定ラインの候補は必ず 2 以上（1 なら射影が全セルを確定させている）ので、分岐は常に本物の選択点だ。解を 2 つ見つけた時点で打ち切る数え上げで、収録 6 盤（6×6〜12×12）すべての解が一意であることを証明している。

盤の生成は答え先行: 辞書から行を 1 本ずつ引いて合法な完成盤を組み（列の均衡は「各色 n/2 以下」を保てば自動で half-half になる）、ヒントをランダム順に一意性が保たれる限り貪欲削除する。残った 1 マス 1 マスが荷重を負っていること——どれを消しても解が 2 つになること——までテストで検査済み。6×6 は 36 マス中 7 個まで削れる。

学び

• ドメインをセルからラインに持ち上げると、局所定石の束が 1 つの射影に潰れる。定石を列挙して実装するより、定石が影として出てくる土台を作るほうが短くて強い
• 大域制約（重複禁止）は持ち上げた途端に alldifferent という既知の形になる
• 39 テスト、TypeScript、ランタイム依存ゼロ。エンジンは約 230 行

コードは全部公開している: https://github.com/sen-ltd/binairo