すべての Griductive パズルは大胆な約束をしています：推測は一切不要。 すべてのマスは論理だけで決定でき、すべてのパズルには唯一の正解があります。
これは設計目標ではなく、数学的な保証です。オペレーションズリサーチやチップ検証で使われるものと同じクラスのソルバーによって強制されています。この記事ではその仕組みを説明します。
なぜ唯一解が重要なのか
パズルに2つの有効な解がある場合、容疑者と無実のどちらでもすべての手がかりを満たすマスが少なくとも1つ存在します。そのマスでは、どれだけ推理しても正解を判断できません——推測するしかないのです。推測は演繹パズルの根本的な契約に反します。
だからこそ、ジェネレーターはたまたま1つの解を持つパズルを生成するだけではありません。パズルが公開される前に、2つ目の解が存在しないことを証明します。
5段階パイプライン
各 Griductive パズルは5段階のパイプラインで構築されます。各段階で何が行われるかを見ていきましょう。
第1段階：ランダムな解を生成
ジェネレーターはまず有効な解のグリッドを作成します——各マスに容疑者または無実をランダムに割り当てます。これがプレイヤーが最終的に推理で導き出すグラウンドトゥルースです。
この時点では手がかりはまだ存在しません。ボードは基本的な構造制約（グリッドサイズ、容疑者数が有効範囲内）を満たすランダムな配置に過ぎません。
第2段階：手がかりプールの構築
次に、ジェネレーターは解のボード上で真となるすべての可能な手がかりを網羅的に列挙します。
Griductive には26種類以上の手がかりタイプがあります——カウント、比較、空間、存在、一意性、連結性など。各タイプについて、ジェネレーターはすべての有効なパラメータの組み合わせをボードに対してテストします。4×4のグリッドでは数千の候補手がかりが生成されることがあります。解に対して真と評価される手がかりだけが保持されます。
これがジェネレーターの原材料です：真の陳述の膨大なプール。その大半は冗長です。
第3段階：最小手がかりセットの選択（最も難しい部分）
ここが本当のコア作業です。ジェネレーターはプールから手がかりの小さなサブセットを選ぶ必要があります。条件は：
- 手がかりが十分である —— それらが合わさって解空間をちょうど1つの有効なボードに制約する。
- 冗長な手がかりがない —— どの1つの手がかりを取り除いても複数の解が可能になる。
ジェネレーターは貪欲制約充足アプローチを使用します：
- 手がかりが選択されていない状態から開始。解空間は完全にオープンで、多くのボードが有効な可能性があります。
- 各候補手がかりを、それが解空間をどれだけ狭めるかでスコアリング。残りの可能性の80%を排除する手がかりは、10%しか排除しないものよりスコアが高くなります。
- 最高スコアの手がかりを選択してセットに追加。
- 更新された手がかりセットで制約モデルを再求解。
- ソルバーが解が1つだけ残っていることを確認するまで繰り返し。
- 刈り込み：最終セットを通して、唯一性の維持に不要な手がかりを削除。これによりパズルがクリーンに保たれ、プレイヤーに余分な情報を与えません。
結果はタイトで公平な手がかりセット——パズルを完全に解くのに十分で、無駄な手がかりがありません。
第4段階：難易度のスコアリング
手がかりセットが確定したら、ジェネレーターはパズルの難易度を0〜100のスケールでスコアリングします。4つの要素が寄与します：
- シンプルな手がかりの比率（35%） —— 直接的なカウントや身元の陳述がどれだけあるか。シンプルな手がかりが多いほどパズルは簡単。
- 複雑な手がかりの比率（30%） —— 多段階や空間推理を必要とする手がかりがどれだけあるか。より深い推理チェーンが求められます。
- 情報の希少さ（20%） —— グリッドサイズに対して手がかりがどれだけ少ないか。手がかりが少ないほど使える情報が少なくなります。
- グリッドの規模（15%） —— 大きなグリッドは本質的に追跡が難しい。5×5パズルは3×3の約3倍のマス数があります。
各手がかりタイプには、求められる推理に基づく固有の複雑さ評価もあります。「Julia は容疑者です」のような手がかりはこれ以上ないほどシンプルです。「Julia は3行目で容疑者の隣人がちょうど1人いる唯一の人物です」のような手がかりは複数のマスをクロスリファレンスする必要があり、はるかに高くスコアリングされます。
第5段階：ヒントの生成と出力フォーマット
最後に、ジェネレーターはヒントシーケンスを構築します——行き詰まったプレイヤーをパズルの中で一歩ずつ導く推奨解法順序です。ヒントは依存の深さで順序付けられます：すぐに推論できるマスが最初に来て、長い前提推理のチェーンが必要なマスは最後に来ます。
最終的なパズルはゲームに必要なすべてのデータとともにパッケージされます：メタ情報、手がかりセット、ヒントシーケンス、難易度スコア。
ソルバー：唯一性の証明方法
パイプラインの中核にあるのは Google OR-Tools CP-SAT です——制約伝播、整数計画法、SAT 求解を組み合わせた制約プログラミングソルバーです。
パズルが数学問題になるまで
グリッド上の各マスはブール変数としてモデル化されます：容疑者（1）または無実（0）。各手がかりは、これらの変数に対する1つ以上の数学的制約になります。
例えば：
- 「3行目にはちょうど2人の容疑者がいる」 は次のようになります：
cell[3,0] + cell[3,1] + cell[3,2] + cell[3,3] = 2 - 「A列のすべての容疑者はつながっている」 は次のようになります：A列の容疑者マスが途切れのない連続した鎖を形成することを保証する連結性制約。
- 「1行目はB列より容疑者が多い」 は次のようになります：
sum(row_1) > sum(col_B)
唯一性の検証方法
手がかりセットを組み立てた後、ジェネレーターは CP-SAT に正確な質問をします：「これらの制約の下で、有効な割り当ては複数存在するか？」
CP-SAT は1つの解を見つけるだけではなく、すべての解を列挙できます。ソルバーがちょうど1つを見つければ、パズルは有効です。2つ以上見つかれば、ジェネレーターは第3段階に戻って手がかりを追加します。
これはヒューリスティックではなく、形式的な証明です。CP-SAT は解空間全体を網羅的に探索します。1つの解があると言えば、まさにちょうど1つ——例外なし。
なぜ総当たりではだめなのか？
5×5のグリッドには25マスがあり、各マスに2つの可能な値があります。つまり2²⁵ = 3300万通りの可能なボードです。すべてを1つずつチェックするのは遅く、スケールしません。
CP-SAT がはるかに高速なのは制約伝播のおかげです：手がかりが「3行目にはちょうど2人の容疑者がいる」と言えば、ソルバーは各組み合わせを個別にチェックすることなく、3行目のすべてのマスの探索空間を即座に縮小します。複雑な手がかりはこの効果を複合的に高めます。実際の運用では、CP-SAT は5×5パズルの唯一性をミリ秒で証明します。
何が問題になりうるか（そしてどう防いでいるか）
「手がかりが曖昧だったら？」
すべての手がかりタイプには厳密な数学的定義があります。「隣人」は常に対角線を含む周囲最大8マスを意味します。「つながっている」は常に隣接するマスの途切れない鎖を意味します。「間」は常に同じ行または列のマスで、端点を含みません。
これらの定義は制約モデルに直接組み込まれています——曖昧さが入り込む自然言語解釈のステップは存在しません。ゲーム内の用語詳細リファレンスは、各空間キーワードの意味をプレイヤーに正確に示しています。
「ソルバーにバグがあったら？」
CP-SAT ソルバーは Google の最適化チームによって保守されている、十分にテストされた広く使用されているツールです。しかし、信頼だけに頼っているわけではありません。生成されたすべてのパズルは独立して検証されます：
- 自動ソルバーがすべてのパズルをステップバイステップで解こうとし、人間のプレイヤーをシミュレーションします。論理的推論だけで完全な解答に到達できなければ、そのパズルはリジェクトされます。
- ヒントの健全性チェックは、シーケンス内の各ヒントが論理的に有効であることを検証します——ヒントされたマスが手がかりと以前に公開されたマスから本当に推論可能であり、隠された情報に依存していないことを確認します。
「手がかり生成がエッジケースを見落としたら？」
各手がかりタイプには形式的な評価関数があり、既知のパズル構成に対してテストされています。手がかりプール生成段階では、実際の解に対して真と評価される手がかりのみが含まれます——解に対して偽の手がかりがパズルに現れることは決してありません。
最終結果
Griductive パズルを開く時、以下のすべてがすでに完了しています：
- ランダムな解が生成された。
- 数千の候補手がかりがそれに対して評価された。
- 最小で冗長性のないサブセットが選択された。
- 形式的ソルバーがそれらの手がかりを満たす解がちょうど1つであることを証明した。
- 自動ソルバーが純粋な演繹でパズルが解けることを独立して検証した。
- 難易度スコアが計算され、ヒントシーケンスが生成された。
すべてのパズル、毎日、4つのグリッドサイズすべてにわたって。例外なし。
行き詰まったなら、まだ十分に活用していない手がかりがあるはずです。2つの答えが可能だと思うなら、手がかりを読み返してください——論理が裁定を下します。証拠が欲しければ、ロジックグラフが手がかりから解答までの完全な推理チェーンを示してくれます。
今後の展望：物語を語る手がかり
現在、Griductive の手がかりは正確な論理的陳述として表現されています——明確で曖昧さはありませんが、確かにやや無機質です。「3行目にはちょうど2人の容疑者がいる」は役割を果たしますが、事件を捜査している探偵の気分にはあまりなれません。
私たちはこれを積極的に変えようとしています。目標は、基礎となる論理的精度を保ちながら、手がかりの表現方法をより多様にすることです。祝日イベントに紐づいた手がかりや、特定の犯罪現場からの目撃証言として構成された手がかりを想像してみてください。無機質な公式ではなく、捜査現場からの本物の証拠のように読めるものになります。
核心的な制約は変わりません：すべての手がかりは一貫性があり、曖昧さがなく、形式的に検証可能でなければなりません。ソルバーは手がかりが数学の教科書のように聞こえるかフィルムノワールの台詞のように聞こえるかを気にしません——論理的な内容だけを見ます。この分離こそが、正確性を損なうことなくより豊かな表現を可能にするのです。
同じ保証。同じ厳密さ。でもパズルは方程式ではなく、解き甲斐のある事件のように感じられるものへ。
推測は不要。運も不要。数学的に保証。