シンメトリーパズル：唯一解保証の盤面自動生成システム紹介

はじめに

こんにちは、株式会社ルーデル所属 26新卒エンジニアの西津（にしづ）と申します。
この記事では、新卒研修のハッカソンで開発した、シンメトリーパズルゲームで使用しているパズル盤面の高速自動生成システムを紹介します。

▼プレイ動画

※動画内サウンド：OtoLogic

対象読者

パズルゲームの自動生成に興味がある方
制約ソルバー（Z3）の実用例を知りたい方
唯一解保証のアルゴリズム設計に興味がある方

目次

はじめに
パズルゲームの概要とルール（ハッカソンで公開したパズルゲームを知らない方はこちらから）
全自動パズル盤面生成システム
生成プロセスの詳細
まとめ

パズルゲームの概要とルール

クリックして展開：ゲームルールの詳細

Kirill（シンメトリーパズルゲーム）

ゲームの基本

プレイヤーは、スタート地点からゴール地点まで一筆書きで線を引いていくパズルゲームです。左右の盤面は線対称となっており、どちらかで引いた線は同期して、もう一つの盤面にも反映されます。

※一筆書きで線を引いて、すべての必須通過点を通りながらゴールを目指します

プレイルール

1. 一筆書きの原則

左右それぞれの盤面で、スタートからゴールまで、途切れることなく1本の連続した線を引く
途中でジャンプしたり、複数の線を引くことは不可

2. 交差と後戻りの禁止

自分がすでに引いた線と交差（クロス）することは不可
一度通った交点や線を再度なぞることは不可（完全な自己回避歩行）

3. グリッド上の移動

線は盤面の縦横の線上のみを通る（斜め移動は不可）

OK：縦横の移動（2×2グリッド）

※右に移動してから下に移動する例

NG：斜め移動（2×2グリッド）

※斜めに直接移動することはできません

4. 必須通過点

盤面上に配置された青い点は必ず通過しなければならない
1つでも逃すとクリア不可

5. 禁止線

通過できない線が盤面に配置されている
これらを迂回しながら正解経路を見つける必要がある

※ 左盤面、Start点から隣への横線を塞ぐ「🚫 禁止線」があるため、下に迂回する必要があります。

デュアルスクリーンとシンメトリー（発展要素）

本ゲームの最大の特徴は、2つの盤面（A・B）を同時に操作する点です。

プレイヤーが盤面Aで線を引くと、盤面Bには鏡写しの線が自動で引かれる
プレイヤーは、両方の盤面の条件を同時に満たす共通の正解経路を見つける必要がある
内部的には「すべての条件が統合された1つのマスター盤面」として判定される

全自動パズル盤面生成システム

ここからが技術的な中身です。盤面の生成には2つの異なるアルゴリズムを使い分けています。

フェーズ	使用アルゴリズム	理由
①正解経路の生成	Z3ソルバー	「長い一筆書き経路を1つ見つける」問題に強い
②唯一解の検証・禁止線の配置	DFS（深さ優先探索）	「解が何個あるか」を正確に数える必要がある

Z3ソルバーとは

概要

Z3は、Microsoft Research が開発したオープンソースのSMT（Satisfiability Modulo Theories）ソルバーです。与えられた論理式や制約条件の集合に対して、それらを同時に満たす解が存在するかどうかを判定し、存在する場合はその具体的な解（モデル）を返します。

動作原理

Z3の基本的な動作は以下の3ステップです。

変数の宣言：解を求めたい未知数を定義する（整数、実数、ブール値など）
制約の追加：変数が満たすべき条件を論理式として記述する
充足判定：すべての制約を同時に満たす変数の割り当て（モデル）を探索する

判定結果は3種類

SAT（充足可能）：すべての制約を満たす解が存在する → 具体的な解を返す
UNSAT（充足不可能）：制約を同時に満たす解は存在しない
UNKNOWN：制限時間内に判定が完了しなかった

本システムでの活用

本システムでは、一筆書き経路の生成を制約充足問題として定式化しています。

変数：path[0], path[1], ..., path[L-1]  （各ステップの座標）

制約：
  ・path[0] = スタート座標
  ・path[L-1] = ゴール座標
  ・すべての path[t] は盤面内（0 ≤ x < サイズ, 0 ≤ y < サイズ）
  ・path[t] と path[t+1] は隣接（上下左右のいずれか）
  ・path[i] ≠ path[j]（i ≠ j のとき）→ 同じ交点を2度通らない
  ・指定した経由点がいずれかの path[t] に含まれる
    ※ゲーム上の「必須通過点」とは別物。経路の形状に多様性を持たせるために
      Z3にヒントとして与える内部パラメータであり、プレイヤーには見えない。

Z3はこれらの制約をすべて満たす座標列を探索し、見つかれば正解経路の候補として返します。見つからなければ経路長を1つ短くして再試行します。（経路長の決定方法）

Z3の内部最適化

Z3は内部で以下のような処理を行い、単純な総当たりよりも高速に解を発見します。

制約伝搬：
ある変数の値が決まると、それに連鎖して他の変数の取りうる値を絞り込む
（例：path[0]がスタート座標に確定 → path[1]はその上下左右の4択に限定される）
矛盾学習：
探索中に「この組み合わせは必ず矛盾する」と分かったパターンを記憶し、同じ失敗を繰り返さない

経路長の決定方法

本システムでは、経路長の探索を以下のように行います。

5×5盤面の場合（全25交点）：

  L=25 で試行 → UNSAT（25マス全部を通る一筆書きは存在しない）
  L=24 で試行 → UNSAT（まだ見つからない）
  L=23 で試行 → SAT ✅（23マスを通る経路が見つかった！）
  → この経路を正解経路として採用

つまり「最長から1マスずつ減らしていき、最初に見つかった経路を採用する」ことで、可能な限り長く複雑な正解経路を得ています。経路が長いほどパズルとしての充実感が高くなります。

スケーラビリティについて：本ゲームの盤面サイズは最大7×7（49交点）です。UNSATの判定は盤面が大きいほど重くなりますが、7×7程度であればZ3のタイムアウト（5秒）内に十分判定が完了するため、この方式で実用上問題ありません。

なぜ全工程をZ3で行わないのか

Z3の得意なこと・苦手なこと

Z3は 「条件を満たす解を1つ見つける」 ことに特化したツールです。
一方で、 「解が全部でいくつあるかを数える」 ことは本質的に苦手です。

問い	Z3の対応	効率
「条件を満たす経路は存在するか？」	SAT/UNSATを返す	◎ 高速
「条件を満たす経路を1つ見つけて」	モデルを返す	◎ 高速
「条件を満たす経路は何個あるか？」	1つ見つける→除外→再度探索→除外→...	✕ 非効率

唯一解の保証には「正解経路以外のルートが1つも存在しないこと」を証明する必要があります。これはZ3に「別解を探して」→「見つかったら除外して、また探して」を繰り返させることで可能ですが、除外制約が増えるたびにソルバーの負荷が指数的に増大します。

DFSが唯一解検証に適している理由

DFS（深さ優先探索）は、すべてのルートを再帰的にたどって列挙する素朴なアルゴリズムです。
唯一解検証では以下の理由で有効です。

早期打ち切り：「解が2つ以上ある」ことが分かった時点で探索を止められる（2つ目を見つけた瞬間に「唯一解ではない」と判定完了）
逐次改善との相性：禁止線を1本追加 → 再検証、のサイクルを高速に回せる
確実性：見落としなく全経路を網羅するため、判定結果に曖昧さがない

DFSの計算量について：DFSの最悪計算量は盤面サイズに対して指数的に増大しますが、本ゲームでは最大7×7に限定されていること、また禁止線や必須通過点の制約により探索空間が大幅に枝刈りされることから、実用上は十分高速に動作します。

結論：適材適所の使い分け

Z3：「長い一筆書き経路を見つける」という探索問題に強い。制約が多いほど有利（絞り込みが効く）
DFS：「解の個数を数える」「2つ目が存在しないことを保証する」検証問題に確実

この2つを組み合わせることで、「複雑で長い正解経路」と「唯一解の数学的保証」の両方を実現しています。

盤面生成システムの全体像

このシステムは、完全自動で唯一解保証のパズル盤面を生成します。

システムの3つの主要フェーズ

フェーズ1：正解経路の生成

Z3ソルバーを使って、できるだけ長く複雑な一筆書き経路を探索

フェーズ2：必須通過点と禁止線の配置

正解経路以外の経路を潰していくことで、唯一解を実現

フェーズ3：唯一解の検証と最適化

DFSで厳密に検証し、不要な禁止線を削除して洗練された盤面に仕上げる

生成プロセスの詳細

ステップ1：Z3ソルバーによる正解経路の生成

Z3が探索した経路の例（4×4グリッド）

※スタート（0,0）からゴール（3,3）まで、縦横の移動のみで長い経路を探索します

Z3に与える制約条件

スタートとゴールを通る
盤面の範囲内を移動（0 ≤ x < サイズ, 0 ≤ y < サイズ）
隣接する交点のみ移動可能（上下左右のみ）
同じ交点を2度通らない（一筆書き条件）
指定された中間経由点を通過

⚠️ 中間経由点について・・・ゲーム上の「必須通過点」とは別物です。

Z3ソルバーは同じ制約条件を与えると毎回同じ解を返す傾向があります。経由点を指定しない場合、スタートとゴールの位置関係から決まる似たような経路ばかりが生成されてしまいます。

これを防ぐために、「途中でこの交点を必ず通れ」というヒントをZ3に与えることで、経路の形状を強制的に変化させています。この経由点はあくまで生成時の内部パラメータであり、プレイヤーには関係ありません。

5つの生成戦略

上記の「経由点をどこから選ぶか」を決めるのが戦略です。

プログラムは、1回の盤面生成でランダムに1つの戦略を選択します。選ばれた戦略に基づいて経由点の候補リストが決まり、そこからランダムに1〜3個が選ばれてZ3に渡されます。同じ試行内では戦略は変わりません。

経由点の個数が1〜3個なのは、制約の強さのバランスを取るためです。

多すぎる場合：Z3に「ここもあそこも通れ」と強く指定しすぎると、すべてを満たす経路が存在しなくなる（UNSAT）リスクが高まる

少なすぎる（0個の）場合：経路の形状にランダム性が生まれず、毎回似た結果になる

1〜3個は「形状に変化を与えつつ、解が見つかる確率を十分に保てる」経験的な調整値です。

盤面サイズが大きくなっても増やさないのか？ → 現段階の実装では盤面サイズに関わらず固定です。盤面が大きいほど解空間に余裕があるため、少ない経由点でも十分に多様な経路が得られます。逆に経由点を増やしすぎると、Z3の探索時間が急激に増大するリスクがあるため、現状は安全策として1〜3個固定を採用しています。

このように、実行するたびに異なる戦略が選ばれるため、同じ盤面サイズでもバリエーション豊かな盤面が生成されます。

戦略名	説明	経由点の選び方
DEFAULT	標準	全交点からランダムに選択
CORNER_FIRST	角優先	四隅（0,0）（4,0）（0,4）（4,4）を優先的に経由
CENTER_FIRST	中央優先	盤面中央付近の交点を優先的に経由
DIAGONAL	対角線	対角線上の交点を優先的に経由
EDGE_WALK	外周	盤面の外周を優先的に経由

ステップ2：必須通過点の配置

正解経路が見つかったら、次は 必須通過点（青い点） を戦略的に配置します。

なぜこの優先順位なのか

ここでの「曲がり角」「直線」は、正解経路上で方向転換しているかどうかの区別です（プレイヤーが見る盤面上の分岐とは異なります）。

この優先順位はプレイヤー体験のためではなく、唯一解を効率的に達成するための内部最適化です。

配置先	優先度	理由
曲がり角（正解経路上）	高い	正解経路が方向転換している交点を必須にすると、別解がその点を避けやすくなる。結果として少ない禁止線で唯一解を達成しやすい
直線上（正解経路上）	低い	直線上の交点は別解もそこを通りやすいため、必須にしても唯一解への貢献度が低い。ただし少量混ぜることで多様性を確保する
トラップペア	最優先	隣接する2点をセットで必須通過点にすると、「直線で繋ぎたいが実際は経路上で遠く離れている」罠が生まれ、別解の排除に大きく貢献する

補足：プレイヤーの体験に影響するのは？

プレイヤーにとっての難しさは、正解経路上の曲がり角/直線ではなく、 実際の盤面でその交点から何方向に進めるか（＝禁止線で塞がれていない分岐の数） で決まります。分岐が多いほど選択肢が増え、惑わされやすくなります。この分岐の数は、後続のステップ3（禁止線の配置）で間接的に調整されます。

曲がり角の例

直線の例

トラップペアとは？

盤面上で隣接しているのに正解経路上では離れている2点のことです。

プレイヤーが、連続で通りたくなるような必須点の配置です。
※必須2と必須3は隣接しているため、連続で通りたくなるが、実際には通ることができない。

トラップペアの盤面配置（4x4グリッド）

クリックして展開：正解経路以外の線を抜いた見やすいバージョン

ステップ3：禁止線の配置と唯一解の実現

別解を潰していくことで、唯一解を実現します。

唯一解実現のロジック

別解の探索方法

DFS（深さ優先探索）で、以下の条件を満たすルートを探します。

スタートからゴールまで到達する
すべての必須通過点を通る
現在の禁止線を通らない
正解経路とは異なるルートである

DFSはスタート地点から再帰的にすべての分岐を探索し、条件を満たすルートを列挙します。正解経路も含めて合計2つ以上のルートが見つかった時点で「唯一解ではない（＝別解が存在する）」と判定し、探索を打ち切ります。見つかったルートが正解経路の1つだけなら「唯一解」です。

禁止線追加の手順

別解を1つ発見：上記のDFSで正解経路とは異なるルートが見つかる
候補の抽出：別解が使っている線と正解経路が使っている線を比較し、別解だけが使っていて正解経路は使っていない線を禁止候補とする。この線を禁止すれば、別解は通れなくなるが正解経路には影響しない
候補をランダムに並べ替え：シャッフルする
連結性を保てる線を1本選ぶ：候補を1本ずつ試し、その線を禁止してもスタートからゴールまで到達可能であることを確認した上で、禁止線に追加する
繰り返し：別解がなくなるまで1〜4を繰り返す

チェック順序による禁止線の違いについて

同じ正解経路であっても、最終的な禁止線の配置は毎回異なります。

手順3でランダムにシャッフルしているため、どの線を最初に禁止するかは実行のたびに変わります。先に禁止した線によって別解の形が変わり、次に必要となる禁止線も変わるため、最終結果はシード値（乱数の初期値）に依存します。

ただし、どの順序で禁止線を追加しても、最終的に「唯一解であること」は必ず検証されるため、パズルとしての正しさは保証されます。

この方式は最適（＝禁止線の数が最小）か？ → 必ずしも最小ではありません。ランダムな順序で禁止線を追加しているため、別の順序ならより少ない禁止線で唯一解を達成できる可能性はあります。ただし、唯一解達成後に不要な禁止線を1本ずつ試し外しする削減フェーズを設けることで、最終的にはなるべく少ない禁止線数に収束させています。

具体例

初期状態：経路が無数に存在。正解経路の線をロックしてそれ以外を抽出（点線）ただしトラップペア（盤面左の二つの必須点）を結ぶ線は除く

抽出した線（点線）をランダムに選定して一旦消してみる（今回は真ん中あたりの線が選ばれた）

正解経路以外で別解があるかDFSで探索

もちろんまだ無数に存在する！別解が見つかったので、選んだ線は削除確定！これらを繰り返す。

上記を何回か繰り返して、今回はこうなった。

DFSで探索. . .

別解が見つからない！正解ルート以外存在しない！唯一解達成！！！
これにより、唯一解が保証された盤面が完成します。

Unity側で取り込まれたあとの見え方

まとめ

このパズル盤面生成システムは、以下の3つの要素を組み合わせることで、唯一解保証のパズル盤面を自動生成します。

システムの強み

✅ 完全自動生成：パラメータを指定するだけで盤面が完成
✅ 唯一解保証：数学的に検証された唯一の正解経路
✅ 多様性：5つの戦略とランダム要素で変化に富んだ盤面
✅ 高速生成：Z3ソルバーによる効率的な経路探索と、解数カウント付きDFSによる高速な唯一解検証の組み合わせにより、実用的な時間で生成が完了する

盤面サイズ	生成時間の目安
5×5以下	約1秒
6×6	約10秒
7×7	1〜3分

※上記の計測環境：会社支給のノートPC（詳細スペックは割愛）

今後の発展可能性

ギミックの追加
難易度の自動評価

すでにいくつかの新ギミックの高速化は実現済み。
またいつか機会があれば、Qiitaに載せようと思っています。

おわりに

最後まで見てくださりありがとうございました。

▼新卒エンジニア研修のご紹介

レアゾン・ホールディングスでは、2025年新卒エンジニア研修にて「個のスキル」と「チーム開発力」の両立を重視した育成に取り組みました。実際の研修の様子や、若手エンジニアの成長ストーリーは以下の記事で詳しくご紹介していますので、ぜひご覧ください！

▼採用情報

レアゾン・ホールディングスは、「世界一の企業へ」というビジョンを掲げ、「新しい"当たり前"を作り続ける」というミッションを推進しています。現在、エンジニア採用を積極的に行っておりますので、ご興味をお持ちいただけましたら、ぜひ下記リンクからご応募ください。