ドスンフワリ(Dosun-Fuwari)を、4 段のソルバー内蔵でブラウザに実装した。ルールの二つの節はどちらも同じ種類の駒しか参照していない——風船を止められるのは上の風船だけ、鉄球を支えられるのは下の鉄球だけ。ここから、盤面の縦の白マス連(run)の中では風船は必ず先頭からの接頭辞、鉄球は末尾からの接尾辞になり、長さ
Lの連の状態はb + s ≤ Lを満たす(b, s)ちょうど(L+1)(L+2)/2通り——三角数 A000217——に潰れる。マスの位置は一切効かない。そして「連の先頭は常に合法な風船置き場」なので、各部屋が run の先頭を 1 個以上持っていれば部屋どうしの選択は完全に独立になり、答えの数はぴったり∏T_i · ∏B_iになる(無飢餓盤 225/225 で一致、飢餓盤 0/650)。つまり一意で非自明な盤は、run の先頭を 1 個も持たない「飢えた部屋」を作るしかない。スタックを一切考えないソルバーは出荷 72 盤すべてで解を 1 つも見つけられない。ソルバー内蔵パズル第 58 弾。
デモ: https://sen.ltd/portfolio/dosun-fuwari/
リポジトリ: https://github.com/sen-ltd/dosun-fuwari
ルール
盤の白マスが部屋に分割されている。各部屋に風船 ○ を 1 個、鉄球 ● を 1 個置く。
- 風船は軽いので浮く。だから風船は、盤の最上行か、黒マスの真下か、別の風船の真下に置く
- 鉄球は重いので沈む。だから鉄球は、盤の最下行か、黒マスの真上か、別の鉄球の真上に置く
以上。黒マスはどの部屋にも属さない。
注目すべきは、どちらの節も 「同じ種類の駒」しか挙げていないことだ。風船を止めるのは黒マス・盤端・風船であって、鉄球ではない。この一語がパズルの形をほぼ全部決めている。
格子は囮で、本体は列の縦連ごとの整数ペア
白マスの極大な縦のつながりを取る。これを run と呼ぶ。定義から run は上下どちらも必ずキャップ(黒マスか盤端)で閉じている。
run の中を見る。風船は「上が黒か盤端か風船」でなければならない。上が空マスの風船はあり得ない。したがって run の中の風船は必ず先頭からの連続した接頭辞になる。同じ議論で 鉄球は末尾からの接尾辞。真ん中は空。
つまり長さ L の run の状態は、風船の個数 b と鉄球の個数 s の組 (b, s)(b + s ≤ L)だけで書き切れる。数えると (L+1)(L+2)/2 通り、三角数だ。
L=1: 3 L=2: 6 L=3: 10 L=4: 15 L=5: 21 L=6: 28 ...
そして 盤全体の配置空間は run ごとの積になる。マスがどこにあるかは効かず、縦の帯の長さだけが効く。8×8 の出荷盤は平均 10.7 本の run を持ち、部屋を一切読まない段階での配置数は約 10^13。12×12 なら 22.2 本で 10^28.4。ソルバーはマスを一度も見ない。run ごとの短いリストを持って、そこから消していくだけだ。
この還元はこのリポジトリで一番重い主張なので、テストは信じずに検証している。1 列だけの盤について 3^L 通りの塗り分けを全部試し、生き残るのがちょうど (L+1)(L+2)/2 個であることを L = 1..9 で確認する。さらに run 還元を一切知らない第 2 エンジン——部屋ごとに風船マスと鉄球マスを総当たりで選び、出来上がった盤をマス単位で検証するだけのバックトラッカ——と突き合わせ、解の個数ではなく解の集合そのものが一致することを見る。
「あるいは他の駒」と言い換えた瞬間、別のパズルになる
このパズルのルールは、しばしば 「黒マス、あるいは他の駒の下」 と短く言い換えられる。風船を鉄球が止めてもよく、鉄球を風船が支えてもよい、という読み方だ。同じことを短く言っただけに見える。
違う。この読み方は、鉄球がその真下の風船に乗っていて、その風船はその鉄球にぶら下がっている——という 2 マスの塊を、下に何も無い宙空で合法にしてしまう。互いが互いの言い訳になっている。
こうなると run の状態は接頭辞+接尾辞ではなくなり、個数は A095263(Pisot 数列 E(3,7)、a(n) = 3a(n-1) - 2a(n-2) + a(n-3))に化ける。
| run の長さ | 公式ルール | ゆるい読み |
|---|---|---|
| 1 | 3 | 3 |
| 2 | 6 | 7 |
| 3 | 10 | 16 |
| 4 | 15 | 37 |
| 6 | 28 | 200 |
| 8 | 45 | 1,081 |
| 12 | 91 | 31,572 |
8×8 で 10^13 が 10^19.2 になる。そしてパズルはその差に耐えない。出荷した 8×8 盤 36 枚のうち、ゆるい読みで一意なものは 0 枚——全部が 5,000 解の打ち切り上限を突き抜けた。正確に数え切れる 6×6 でやり直しても、一意だった 40 枚が 一意 0 枚になり、その中で解が一番少ない盤ですら 3,264 通りあった。
ゆるい言い換えはパズルを易しくしていない。消している。
リポジトリはこの事実をもう一つ別の書き方でも持っている。ungroundedCount は各駒の支持連鎖を不動点で辿り、それがキャップに着地するかを見る(局所条件ではなく物理的な「settle するか」の読み)。公式ルール下ではこれが常に 0で、合法な配置に宙に浮いた駒は一つも存在しない——テストがそれを主張している。ゆるい読みでは 2 マスの反例で両方の駒が ungrounded になる。
run の先頭は常に合法な風船置き場、そこから全部が決まる
run の先頭マスはキャップに直接寄りかかっている。だからそこに風船を置くのは、盤の他がどうなっていようと常に合法だ。末尾マスと鉄球も同じ。
ここで数える。もしすべての部屋が run の先頭を 1 個以上含んでいるなら、各部屋は自分の持っている先頭マスの中から風船を勝手に選べる。他の部屋が何をしても干渉されない。選択は完全に独立で、部屋 i が先頭を T_i 個・末尾を B_i 個持つ盤の解の数は、ぴったり
∏ T_i · ∏ B_i
になる。
これは予言なので、仮定せずに測った。飢餓部屋のない盤 225 枚のうち 225 枚が予言どおりの解数を持ち、それを超えたものは 0 枚。逆に飢餓部屋のある盤 650 枚では 0 枚しか一致しなかった。端で徐々に崩れる近似ではなく、別のレジームだ。
ここから、このパズルの設計問題そのものが出てくる。一意にするには全部の項が 1 でなければならない。つまりどの部屋もちょうど 1 個の run 先頭と 1 個の run 末尾を持つ、つまり部屋の数=run の数。ところがそのとき答えは「run の先頭は全部風船、末尾は全部鉄球」であり、部屋を一切読まずに書き下せてしまう。
一意性と面白さが正面から衝突する。抜け道は一つしかない。ある部屋を 飢えさせる(starve) ことだ。run の先頭を 1 個も与えない。するとその部屋の風船は**別の部屋にある風船の上に積む(stack)**しかなくなり、その要求が隣の部屋まで伸びて、隣の選択まで固定してしまう。
出荷盤は全部この作りだ。8×8 は飢餓部屋の中央値 3、12×12 は 6。アブレーションは無愛想なほど明快で、同種の駒を積むことを一切考えないソルバーは、出荷 72 盤すべてで解を 1 個も見つけられない(72/72 が解無し)。
ダイヤルは飢餓部屋の数
生成器はまず自明な盤を引く——run 1 本につき部屋 1 個。これは常に一意で、常につまらない。そこから部屋を 1 個ずつ飢えさせる。ある run の先頭マスを隣の部屋に渡すと、残された部屋は先頭を失って積むしかなくなる。飢えさせるたびに一意性を失う危険が増える。
| 飢餓部屋 | 8×8 引いた数 | 一意 | 率 |
|---|---|---|---|
| 0 | 220 | 220 | 100.0% |
| 1 | 220 | 200 | 90.9% |
| 2 | 220 | 185 | 84.1% |
| 3 | 216 | 157 | 72.7% |
| 4 | 153 | 112 | 73.2% |
律速は一意性の率ではなく引けるかどうかだった。8×8 では 4 個を超えると「十分長くて隣接している run」が尽きる。だから 8×8 の出荷盤は 4 で止めてある。12×12 は run が 22.2 本あるので 8 個まで届き、そこでもまだ 55.1%。
ランダムな盤には解が無い
黒マスをランダムに撒き、白マスをランダムな連結部屋に切って、解を要求してみる。
| 盤 | 黒率 | 引いた数 | 解無し | 一意 | 複数 |
|---|---|---|---|---|---|
| 6×6 | 0 | 600 | 600 | 0 | 0 |
| 6×6 | 0.12 | 600 | 594 | 0 | 6 |
| 8×8 | 0 | 600 | 600 | 0 | 0 |
| 8×8 | 0.12 | 600 | 599 | 0 | 1 |
| 8×8 | 0.20 | 600 | 596 | 0 | 4 |
| 10×10 | 0.15 | 600 | 600 | 0 | 0 |
3,600 枚中 3,589 枚が解無し、一意は 0 枚。 各部屋は「接頭辞で届くマス」と「接尾辞で届くマス」の両方を持たなければならず、ランダムな部屋はそれを満たさない。
だから生成器は答えを先に描く。そして配置ルールを一度もチェックしない——置くのは常に run の先頭(風船)と末尾(鉄球)だけで、それは位置だけで合法だからだ。チェックするのは一意性、つまり実際に不確かな唯一のものだけになる。
ラダー
4 段。すべて同じ run ごとのドメイン上で動く、狭義に強くなっていく伝播器。
-
run— run の状態表だけ。伝播なし -
room— 部屋あたり風船 1・鉄球 1。同種 2 個を 1 部屋に落とす run 状態は死に、1 本の run しか供給できない部屋はその run を確定させる -
profile— ある部屋で駒が確定すると、その run 全体が切れる。run の他のマスは、触れている全部屋でその選択肢を失う -
probe— 単一化整合性。run 状態を 1 つ仮定して伝播し、それだけで矛盾するなら落とす
段の切れ目が上の構造とぴったり一致した。飢餓部屋の無い盤 150 枚は 150 枚とも room で終わる——数えるだけ、浮くとか沈むとかの話は一度も使わない。そして出荷 72 盤は 72 盤とも profile を要求し、probe も探索も 1 枚も必要としない。部屋を 1 個飢えさせると盤はきっかり 1 段上がり、それ以上は上がらない。
生成器の詰まりどころ
最初に書いた生成器は素直だった。ランダムな配置を引いて、部屋を描いて、一意になるまでやり直す。これがまったく動かない。
- 部屋を先に引くと 3,600 枚中 3,589 枚が解無し
- 答えを先に描いて部屋を後から流し込むと、今度は解が数十個出る
- 「風船パッチ」と「鉄球パッチ」の二部マッチングで部屋を組む案は、150 枚中 150 枚でマッチングが存在しない。風船は上に、鉄球は下に層をなすので、風船パッチの周りには風船パッチしかいない
- 部屋の空きマスを隣に渡す山登りで一意性まで詰める案も 0/25。渡せる相手がいない内部マスに曖昧さが居座る
行き詰まってから上の ∏T_i · ∏B_i を計算して、それまでの全部が同じ理由で失敗していたことがわかった。部屋がそれぞれ run 先頭を持っている限り、選択は独立で、積は絶対に 1 にならない。曖昧さは「詰めが甘い」のではなく構造的に消せない。飢餓部屋という概念に辿り着いた時点で、生成器は数行になった。
まとめ
- ルールの節が同じ種類の駒しか見ていない。だから run の中で風船は接頭辞、鉄球は接尾辞になり、run の状態は三角数 A000217 個に潰れる
- 「あるいは他の駒」というゆるい言い換えは、宙に浮いた相互支持ペアを合法にし、状態数を A095263 に変え、出荷盤の一意性を 36/36 から 0/36 に落とす
- run の先頭は常に合法な風船置き場。よって飢餓部屋の無い盤の解数はぴったり
∏T_i · ∏B_i(225/225 で一致) - したがって一意で非自明な盤は、run 先頭を 1 個も持たない部屋を作り、スタックを強制するしかない。スタックしないソルバーは出荷 72 盤で 0 解
- ラダーの切れ目がこの構造と一致する。無飢餓盤 150/150 が
room、出荷 72/72 がprofile、probeと探索は 1 枚も要らない
ソルバー内蔵パズル第 58 弾。テスト 21 本、ランタイム依存ゼロ。
