チョコバナナを解く — 「〜でない」としか言えないルールのほうが、外すと6倍高くつく

Posted at 2026-09-02

チョコバナナを、5 つのルールセット内蔵でブラウザに実装した。塗ったマスの塊は必ず長方形、塗らないマスの塊は決して長方形でない。同じ述語を、肯定で 1 回、否定で 1 回。ソルバー内蔵パズル第 52 弾。

デモ: https://sen.ltd/portfolio/choco-banana/
リポジトリ: https://github.com/sen-ltd/choco-banana

ルール

H×W の盤面のいくつかのマスを塗る。

塗ったマスの連結した塊は、必ず長方形（チョコ）
塗らないマスの連結した塊は、決して長方形でない（バナナ）
マスの中の数字は、そのマスが属する塊の大きさ。その塊が何色かは一切言わない

ルール 1 と 2 は同じ述語だ。片方は肯定され、片方は否定されている。そしてルール 3 は面積を渡して色を伏せる。この 2 つの非対称が全部で、測れるのもこの 2 つだ。

推論としての 2 方向は、まったく等価でない

「長方形である」は外接矩形について閉じている。 同じ塊にあると分かっている塗りマスは、その外接矩形を丸ごと引きずり込む。だから 2 マスが 1 ブロックを埋める。これは押すルールだ。

「長方形でない」は何についても閉じていない。 いま長方形になっているバナナは、まだ違反ではない。封じられて、もう成長できなくなった瞬間に初めて違反になる。だからこのルールは局面を進められない。棄却しかできず、しかも最後の最後にしかできない。

そう書くと、否定のほうが安い半分に見える。そうではなかった。

ソルバーが書き込んだマス 1 つ 1 つを、書いた段に帰属させる（出荷している 68 盤）:

サイズ	盤数	`value`	`rect`	`size`	`anti`	`probe`
6×6	38	19.8%	5.5%	62.6%	4.2%	7.9%
8×8	30	15.3%	3.5%	67.4%	4.5%	9.2%

長方形述語の 2 つの半分は、書くマス数がほぼ同じで、どちらも塊サイズの算術 (size) に食われている。ところが全段から 1 段ずつ抜くと、損失は逆向きに偏る:

変種	確定率	推測なしで完走	仮定回数
全段	100.0%	68/68	0
− `value`	86.7%	50/68	332
− `rect`	97.2%	54/68	498
− `anti`	89.8%	36/68	11,686
− `size`	23.5%	8/68	3,623,318

probe を載せない状態で比べると、− rect は 17,452 仮定、− anti は 103,958 仮定。「いいえ」しか言えないルールのほうが、「はい」と言えるルールより 6 倍高い。

なぜそうなるか

肯定の半分は、すでに引っ越しているからだ。

その本体は size 段の中で働いている。面積 v の手掛かりが付いたチョコの塊は、「まだ入る面積 v の長方形」の集合と突き合わせられ、全候補に共通するマスは塗られ、塊に接しているのにどの候補にも入らないマスはバナナになる。これは**数字が付いた「長方形である」**そのものだ。だから rect 単体には、もうほとんど仕事が残っていない。

否定の半分には、そういう第二の住所が無い。

（− size の行の「一意 10/68」は、探索が仮定 6 万ノードの予算を 58 盤で使い切ったという意味で、答えの数が変わったわけではない。予算切れ自体がコストの測定になっている。）

ルールとして外すと、今度は両方が効く

段としてではなくパズルのルールとして片方を落とすと、話が変わる。一意性は段の性質ではなくルールの性質だからだ。

サイズ	盤数	全ルール	「バナナ≠長方形」なし	「チョコ=長方形」なし
6×6	38	38/38	12/38	21/38
8×8	30	30/30	12/30	9/30

「バナナは長方形でない」を落とすと、6×6 で 38 盤中 26 盤、8×8 で 30 盤中 18 盤が一意でなくなる。中央値で 2 個・4.5 個の答えが湧く。逆に 8×8 では「チョコは長方形」を落とすほうが痛い（9/30）。制約としては、どちらの半分も等しく骨組みだ。 差が出るのは推論として使うときだけで、そのときは否定のほうが高い。

数字は量ではなく因数分解

手掛かりは面積を渡して色を伏せる。だから読むのは算術の問題になる。

連結した 1 マスまたは 2 マスの集合は、どう描いても長方形だ。よって 1 と 2 は必ずチョコ。
面積 v のチョコは、H×W 盤では v = a·b（a ≤ H, b ≤ W）のときにしか存在しない。この掛け算表に無い数字は必ずバナナ。6×6 盤なら 7, 11, 13, 14, 17, 19, 21, 22, 23, 26… が全部そうだ。

そして面積 v のバナナは 3 ≤ v ≤ H·W − 1（H, W ≥ 2）のときちょうど存在する。両端がまさに長方形を強制するケースで、その間は全部構成できる: ⌊v/W⌋ 行を丸ごと取り、余りを次の行に置く。余りが 0 のときは最後の行から 1 マス削って下にぶら下げればよい。

つまり value 段は盤面を一切見ない。数字と盤のサイズだけで色が決まる。

v	6×6	8×8	10×10
1, 2	チョコ	チョコ	チョコ
7	バナナ	どちらでも	どちらでも
11, 13	バナナ	バナナ	バナナ
14	バナナ	どちらでも	どちらでも

ありうる塊サイズのうち、自分の色を名乗ってしまうものが半分以上ある: 6×6 で 36 個中 21 個 (58.3%)、8×8 で 64 個中 37 個 (57.8%)、10×10 で 100 個中 61 個 (61.0%)。出荷盤でも 6×6 の手掛かり 388 個のうち 271 個 (69.8%) が名乗る側だった（内訳: 「1 か 2」が 195 個、掛け算表の外が 76 個）。

n×n 盤でチョコが取りうる面積の個数は OEIS A027424 そのもの: 1, 3, 6, 9, 14, 18, 25, 30, 36, 42。

手掛かりでは絶対に区別できない答えがある

チョコバナナの手掛かり言語は、正確に**「マス → その塊の大きさ」という写像**だ。だから存在しうる最強の手掛かり集合は「全マスに数字を書く」であり、そこから 1 行で定理が出る。

答え A を一意にできる ⟺ A のサイズ写像を持つ合法な盤が A だけ。

（⇐）唯一なら全マスに書けば一意。（⇒）別の答え B が同じサイズ写像を持つなら、B は A が満たす手掛かりを全部満たす。どんな手掛かり集合も B を落とせない。

そして右辺は常には成り立たない。3×4 盤で、2×3 のチョコを 4 隅のどこに置いても、残る 6 マスのバナナは L 字になる。4 つとも、全マスが 6 を読む。

###.     .###     ....     ....
###.     .###     ###.     .###
....     ....     ###.     .###

12 個の数字を全部書いても、答えは 4 つ立ったままだ。

全数え上げの結果:

盤	答え	相異なるサイズ写像	引き分けに巻き込まれた答え	最大の組
2×2 … 3×3	5 … 121	全部相異なる	0 (0.0%)	1
3×4	599	596	4 (0.7%)	4
3×5	3057	3055	4 (0.1%)	2
4×4	4835	4831	8 (0.2%)	2
4×5	40899	40875	48 (0.1%)	2

3×3 以下には 1 組も無く、3×4 で初めて現れて、以後 0.1% 前後で居座る。生成器はこれを検出して降りる必要がある——敵対的に手掛かりを買うループが、2 つの答えが食い違うマスを 1 つも見つけられなくなった時点で null を返す。

手掛かりの方言

「自分の色を名乗る数字だけ」「名乗らない数字だけ」に制限して買ってみると、どちらの方言も不完全だった:

サイズ	盤数	制限なし	名乗る数字だけ	黙る数字だけ	値段（中央値）
6×6	38	38	19	15	6.0 / 7.0 / 8.0

制限なしなら 38 盤全部を一意にできるが、名乗る数字だけでは 19 盤、黙る数字だけでは 15 盤しか組めない。値段（最小手掛かり数の中央値）は 6 / 7 / 8 とそれほど変わらないので、負けているのは値段ではなく存在のほうだ。

`probe` は健全だが完全ではない

前作（ヤジサンカズサン）では「probe が推測なしで完走する」と「答えが 1 個」が 718 接頭辞で 1 件も食い違わなかった。今回は違う。

検査した手掛かり接頭辞: 581
一致: 525 (90.4%)
一意なのに probe が止まった: 56
probe が完走したのに一意でない: 0

ずれは片側にしか出ない。 probe が「終わった」と言った盤が実は複数解だった、という事故は 1 件も無い（そうでなければソルバーのバグだ）。一方で、答えが 1 個しかないのに probe では推測が要る盤が 56 回あった。パズルの難易度と探索の強さは、ここでは別物だった。

出荷している手掛かり集合はすべて極小だ。一意性用の手掛かり 518 個を 1 つずつ抜いたところ、一意のまま残ったものは 0 個、抜くと中央値 26 個の答えが湧いた。

台帳

手掛かりが 1 つも無い盤の答えの数（3 エンジンが一致した値）:

盤	答えの数
`n×n`, n = 1…5	1, 5, 121, 4835, 584931
`1×n`	1, 1, 1, 1, 1, 1, 1, 1
`2×n`, n = 1…10	1, 5, 19, 57, 171, 509, 1505, 4441, 13105, 38689
`3×n`, n = 1…8	1, 19, 121, 599, 3057, 15525, 78781, 399575

どれも OEIS に無い（2026-09 時点）。1×n が全部 1 なのは偶然ではない: 帯の連結部分集合はどれも長方形なので、バナナが 1 つも住めない。よって答えは「全部チョコ」の 1 通りだけになる。

外部と接している数はもう 1 つ、掛け算表のほう（A027424）だ。

3 つのエンジン

コードを 1 行も共有しない 3 つの実装が、すべての盤で一致しなければならない:

solveCtx — 伝播つき探索
bruteByMask — 盤を整数だと思って全部試す
bruteByCells — 読み順にマスを走査し、最後の隣接マスが決まった瞬間に塊を封じて判定する

出荷盤で solver 対マス走査が 67/67、3 エンジン全部が回る小さい盤で 100/100 一致。テストは 72 本。

開発中に実際にこれで捕まったバグが 1 つある。anti 段が「白の連結成分リストを最初に作ってから、ループの中でマスを書き込む」実装になっていた。書き込みは 2 つのバナナを併合しうるので、リストの後ろの成分は古くなる。古い成分は本物の部分集合なので「もう出口が無い＝封じられた長方形」に見えてしまい、正しい答えを矛盾として棄却していた。マス列挙エンジンが 1 盤で solver=0, brute=1 を出して発覚した。修正は「書き込んだら即 'changed' を返して外側のループにやり直させる」の 1 行。回帰テストも 4×4 の最小例で入れてある。

5 段のはしご

段	内容
`value`	数字だけで色が決まる: `1`/`2` はチョコ、掛け算表の外はバナナ
`rect`	チョコの塊は外接矩形を埋める
`size`	手掛かりの塊はちょうどその大きさ: 下限（今ある分）と上限（届く範囲）の両方が飽和する + チョコなら生き残る長方形配置の共通部分
`anti`	バナナは長方形でない: 封じられた長方形は矛盾、出口が 1 つならそこはバナナ、四方を囲まれたマスはチョコ
`probe`	単一セル整合性

累積の確定率（6×6）は 19.8% → 34.4% → 69.7% → 79.8% → 100%。

まとめ

同じ述語の肯定と否定は、推論としては等価でない。だが安いのは否定のほうだ、という直感は逆だった: 外すと 6 倍高い
理由は肯定の半分が size 段に引っ越しているから。rect 単体はほぼ空箱
ルールとして落とすと両方が骨組み。6×6 で 26 盤、8×8 で 18 盤が一意性を失う
手掛かり言語 = サイズ写像。だから一意化できる ⟺ サイズ写像が唯一。3×4 の 4 隅で反例が出る
1 と 2 は必ずチョコ、掛け算表の外は必ずバナナ。ありうるサイズの半分以上が自分の色を名乗る