はじめに：AI時代の「ものづくり」
最近のAI、進化が早すぎませんか？
毎日のように新しいモデルが出てきて、「ゲーム作ってみた」「アプリ作ってみた」という記事を見るたびに、エンジニアとしての血が騒いでいました。
「自分もAIを使って何か作りたい。どうせなら、昔から好きなパズルで。」
私は 「ナンバーリンク」 という、盤面上の同じ数字同士を線で結ぶパズルが大好きです。
かねてから「このパズルを自動で解いたり、あるいは無限に自動生成するプログラムを作りたい」と思っていました。
これまでは「アルゴリズムどうしよう、バックトラック法とかか……？ 実装が面倒だ……」と腰が重かったのですが、「今のAIなら、設計から実装まで全部丸投げしてもいけるのでは？」 と思い立ち、Geminiを相棒（というか主戦力）に開発を始めてみました。
結論から言うと、自分では思いつかなかった「SATソルバー」というガチな数学的アプローチを提案され、実装まで完走できました（そして最後に、AIだけでは越えられない壁にもぶつかりました）。
AIとのペアプロ開始
1. とりあえず要望を投げる
まずは雑に、やりたいことを投げました。
私: 与えられた、ナンバーリンクというペンシルパズルの問題を解くソルバープログラムを開発したいです。最適なアルゴリズムなども、あれば教えてください。
すると、AIは即座にこう返してきました。
AI: ナンバーリンクはNP完全問題として知られており、制約プログラミングやSATへの還元が、特に難易度の高い問題を解くのに有効な手段です。SATソルバー（充足可能性問題ソルバー）を用いて解くのが有効なアプローチです。Pythonの
python-sat(PySAT) ライブラリを使用するのが標準的で高速です。
お、おう、なるほどなー、充足可能性問題なー！ わかるわー完全に理解した。
そして、頼んでもいないのに「変数の定義」「制約条件の数式化（CNF化）」、そして「実装コード」まで一気に出力してきました。
2. SATソルバー？ なにそれ？
正直、私は数学や数理モデル構築の専門家ではありません。「なんか速いらしい」くらいの知識でした。
しかしAIの説明によると、ナンバーリンクは以下のような論理パズルとして記述できるそうです。
- 色の変数 ($C_{i,j,k}$): マス $(i, j)$ に数字 $k$ が入るか？
- 接続の変数 ($E_{u,v}$): マスとマスが繋がっているか？
-
制約:
- 「隣り合うマスが繋がっているなら、色は同じでなければならない」
- 「数字のマスは端点なので線は1本だけ」
- 「空白マスは線が通るなら2本（入って出る）、通らないなら0本」
これらを「論理式（CNF）」に変換し、ソルバーに食わせると、答えが一瞬で出る。
なるほど、バックトラックで再帰関数をカリカリ書くより、数理モデルに落とし込むほうが賢いのか。AI、やるじゃん。
3. バグ発生、そして修正もAI任せ
最初に出力されたコードを実行してみると、何を投げても No solution foundに。どうやら何かがおかしい。
ここでも、自分でデバッグプリントを仕込むのではなくAIに丸投げします。
私: 「問題が全く解けないんだけど、なんで？」
AI: 「解析しました。どうやらライブラリの変数ID管理にバグがあったので直します」
すごい。
「論理的な制約のミス」と「ライブラリの使い方のミス」を同時に修正したコードが返ってきました。人間がやったら半日は溶ける作業です。
完成したコード（抜粋）
最終的に出来上がったソルバーのコア部分（のよう）です。
実際、ソースを全文解読はできていないです（エンジニア失格か）。
GitHubリポジトリとして公開しました：
mashinosatoshi/pencil_puzzle_solver
def _generate_constraints(self, force_full_fill):
for r in range(self.rows):
for c in range(self.cols):
# ... (色の制約などは省略) ...
# 次数制約（ここが肝）
if self.grid[r][c] != 0:
# 端点: 次数は必ず 1
self.add_clauses(CardEnc.equals(lits=adj_edges, bound=1, top_id=self.next_var-1))
else:
# 空白マス
if force_full_fill:
# 全マス埋め問題の場合: 次数は必ず 2
self.add_clauses(CardEnc.equals(lits=adj_edges, bound=2, top_id=self.next_var-1))
else:
# 空白許容の場合: 次数は 0 または 2 (1は禁止、3以上も禁止)
# (A) 次数は2以下
self.add_clauses(CardEnc.atmost(lits=adj_edges, bound=2, top_id=self.next_var-1))
# (B) 次数は1ではない (入ってきたら必ず出る)
if len(adj_edges) > 0:
for i, e_target in enumerate(adj_edges):
others = adj_edges[:i] + adj_edges[i+1:]
if others:
# e_target が True なら、others のどれかも True
self.cnf.append([-e_target] + others)
else:
self.cnf.append([-e_target])
実行結果
Webで見かける形式のテキストデータを食わせてみます。
入力:
. . 4 . . .
. . . . 2 .
. 3 . . . 3
. 1 2 4 . .
. . . . 1 .
. . . . . .
出力:
[4, 4, 4, 3, 3, 3]
[4, 3, 3, 3, 2, 3]
[4, 3, 2, 2, 2, 3]
[4, 1, 2, 4, 4, 4]
[4, 1, 1, 1, 1, 4]
[4, 4, 4, 4, 4, 4]
（※実際は数字ではなく線を可視化したほうが分かりやすいですが、ロジック上は正しく線が繋がっています！）
一瞬です。試しに10×10の一般的な難易度のものを投げてみても、すぐに答えが返ってきました。
自分でアルゴリズムを考えていたら、まだ「再帰が止まらない」と悩んでいたことでしょう（そもそもコーディングにまでたどり着けていなかった可能性すら）。
残された課題：25×25 ジャイアントパズルの壁
さて、ここまでは順風満帆でした。
「AIすごい！SATソルバー最強！もう全部これでいいじゃん！」
そう調子に乗った私は、ネットで見つけた 「25×25」の超巨大ナンバーリンク（ジャイアントパズル） をこのソルバーに投げてみました。
人間が解けば数時間はかかる代物です。AIなら数秒で終わるでしょう。
……返ってこない。
1分経過。
5分経過。
ファンが唸りを上げ、CPU使用率は100%に張り付いていますが、答えが出ません。
結局、10分待っても結果は返ってきませんでした。
なぜ解けないのか？
どうやら、盤面が大きくなると変数の数（マス数 × 色数）と制約条件（Clause）が爆発的に増えてしまい、今の「ナイーブな（単純な）SATエンコーディング」では探索空間が広すぎて太刀打ちできないようです。
AIに「作って」と丸投げしたコードは、正しくはあるものの「最適化」までは考慮されていませんでした。
ここから先は、
- 不要な変数の削減（前処理）
- より高度な制約の追加（ループ禁止の効率化など）
- あるいはSATではなくZDD（Zero-suppressed Binary Decision Diagram）のような別アルゴリズムへの移行
といった、「人間のエンジニアによるチューニング」 が必要になりそうです。
おわりに
AIは「0から1」を爆速で作ってくれましたが、「1を100にする」高速化や最適化の領域には、まだ我々が手を動かす余地（楽しみ）が残されていました。
とはいえ、たった数十分で「動くソルバー」が手に入ったのは事実です。
このベースラインがあるからこそ、「じゃあどう高速化するか？」という次のステップに進めます。
次は、この「25×25の壁」を超えるべく、AIと相談しながら高速化に挑んでみたいと思います。
GitHubリポジトリ（記事作成時点コミット）:
https://github.com/mashinosatoshi/pencil_puzzle_solver/tree/bd1a22114a8c71b6990bfaccedef32da5d577f8a
※この記事もGeminiを使用して作成しています。