0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

ドスンフワリ — ルールが「同じ種類」しか見ていないので、盤は列の縦連ごとの整数ペア 1 個に潰れる

0
Posted at

ドスンフワリ(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

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^1310^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 が profileprobe と探索は 1 枚も要らない

ソルバー内蔵パズル第 58 弾。テスト 21 本、ランタイム依存ゼロ。

0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?