はじめに：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}$): マスとマスが繋がっているか？
制約:

これらを「論理式（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を使用して作成しています。