美術館（Akari / ライトアップ）を制約伝播で解く — 壁数字則・相互可視則・点灯則の不動点伝播、最暗マス探索、解の一意性を証明するパズル収録

光を灯すパズル 美術館（Akari / ライトアップ） を、制約伝播ソルバー内蔵でブラウザに実装した。勘所は 3 つ: (1) 3 つの健全な規則を不動点まで伝播 — 壁の数字則・相互可視則（電球は互いを照らせない）・点灯則（暗いマスの最後の光源が 1 マスなら電球に確定）はどれも推測ではなく含意、(2) 論理が詰まったら「最も暗いマス」から探索 — 候補が最少の暗いマスで分岐し、解を数え上げて一意性を証明する、(3) 収録 5 問は「壁配置」だけを与える — 手がかりも答えもソルバーが導出するので、絵と答えが構造的に食い違わない。ソルバー内蔵パズル第 7 弾。

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

ルールと、なぜ論理で解けるのか

盤面は白マスと壁（黒）でできていて、壁の一部に 0..4 の数字が入る。プレイヤーは白マスに電球を置く。電球は自分のマスを照らし、行と列に沿って最初の壁に当たるまで光を飛ばす。解の条件は 3 つ:

1. 点灯 — すべての白マスが照らされる
2. 相互不可視 — どの電球も、別の電球の光線上に置かれてはいけない
3. 壁の数字 — 数字付きの壁は、隣接する電球がちょうどその数だけ

この 3 つがそのまま**厳密な含意（推測ゼロ）**の推論規則になる:

• 壁数字則 — 隣の電球数が数字に達した壁は、残りの隣接白マスを電球不可にする。逆に「残りの空きマスを全部電球にしないと足りない」なら、それらは全部電球。
• 相互可視則 — 電球は自分の光線上のマスをすべて電球不可にする（同じ光線上に電球が 2 つあれば即矛盾）。
• 点灯則 — まだ暗い白マスについて、それを照らせる候補（自分自身＋光線上の未確定マス）が残り 1 つなら、そこは電球に確定。0 なら矛盾。

if (bulbs > w.n) return { ok: false, forced };  // 壁が過剰 → 矛盾
if (count === 0)  return { ok: false, forced };  // 二度と照らせない → 矛盾
if (count === 1)  set(candidate, BULB);          // 最後の光源に確定

propagate() はこの 3 規則を不動点まで回し、確定した順番を記録する。デモの Hint はこの「手がかりだけから強制される 1 手」を再生する（勘なし）。

論理が詰まったら: 一意性まで証明する探索

盤面によっては最後に推測が要る。バックトラッキングは**「最も暗く、電球候補が最少のマス」（点灯制約に対する MRV）を選び、電球を置いてみて伝播に枝を刈らせる。ここで効いてくる不変条件がある——伝播後、照らされたマスはすべて電球不可に落ちている（相互可視則）。だから残った未確定マスは必ずまだ暗いマス**であり、探索は「光が本当に足りない場所」でしか分岐しない。無駄な分岐が構造的に消える。

function chooseCell(state, g) {
  let best = -1, bestCount = Infinity;
  for (const i of g.whites) {
    if (state[i] === BULB || isLit(state, g, i)) continue; // 既に明るいマスは飛ばす
    // i を照らせる未確定候補を数え、最少のものを選ぶ
    ...
  }
  return best;
}

hasUniqueSolution は解を 2 つまで数え上げ、テストは収録全問が「ちょうど 1 つ」で止まることを要求する。倉庫番(#286)・ノノグラム(#287)・スリザーリンク(#288) と同じ「レベルはソルバーを通してから出荷」の思想だ。

収録問題は「壁配置」が single source of truth

各問は 壁配置だけ（# と .）で書く。手がかりの数字も答えもソルバーが作る:

1. 数字なしで壁配置を解く。点灯則と相互可視則だけで妥当な電球配置 S が 1 つ求まる。
2. すべての壁に S から数字を振る。この完全手がかり盤が一意であることを要求する（そうでなければ盤面を却下）。
3. 一意性が保たれる範囲で数字を貪欲に空欄化し、推理の余地を残す。

こうすると「絵（壁配置）」が唯一の真実で、答えはソルバー自身の出力なので、両者が食い違いようがない。テストは仕上がった盤を解き直して電球が S と一致することを確かめる:

expect(hasUniqueSolution(b.puzzle)).toBe(true); // 解はちょうど 1 つ
expect(bulbsFound).toEqual(bulbsWant);          // しかもそれが S

収録 5 問（7×7〜10×10、いずれも 180° 回転対称）はこうして自動生成した。デモの Solve は求めた唯一解の電球を 1 つずつ灯していくので、暗い部屋に光が満ちていく。トップ画像は 10×10「Gallery」が解けた瞬間だ。

まとめ

美術館は 3 つの健全な規則の不動点伝播 でかなり進み、詰まったら 最暗マスからの探索が一意解を証明して仕上げる。ソルバー内蔵パズルはこれで 7 本目——数独 / ライツアウト（GF(2)）/ 15パズル（パリティ+IDA*）/ 倉庫番（pull-BFS）/ ノノグラム（制約伝播）/ スリザーリンク（辺の制約伝播）/ 美術館（点灯制約の伝播＋一意性証明）。それぞれ違う数学を着ている。デモで部屋に光が満ちる瞬間をぜひ。

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