🚀はじめに
数理最適化を活用した「🐧アニマル数独アプリ」を作成しました。最近業務で数理最適化を活用しているのですが、機械学習などのデータドリブンなAIと比べて認知度が低く、一から説明することが多いです。その説明の導入時に「🐧アニマル数独アプリ」が使えるのではなかろうか！といった思いが開発の動機です。そんな背景もあって、今回は特にアルゴリズムの部分に焦点を当てて解説しようと思います。
⛓リンク
🌐ウェブサイト
Streamlit Cloud にデプロイしたアニマル数独アプリのQRコードです。以下の画像をクリックするかスキャンして、ウェブサイトにアクセスできます！
🐱リポジトリ
- 🐧アニマル数独アプリ
Streamlit Cloud にデプロイしたのはこちらのリポジトリです。
- 🔢数独ソルバー
上記のアニマル数独アプリから、数理最適化のアルゴリズムの部分のみを抽出したリポジトリです。
🧑🏻💻開発言語・ライブラリ
🐍Python
数独のアルゴリズムからウェブアプリケーションまですべて Python で開発しました。
👑Streamlit
Web フレームワークは Streamlit を採用しました。HTML, CSS, JavaScrip を使わずに Python のみでWebアプリを作成できます。2022年に Snowflake に買収されており、コミュニティが活発で、頻繁に機能がアップデートされています。専用のサーバーがあり、作成したアプリケーションを簡単にデプロイできる点もモダンです。Flask, Django と比べて、それなりのものをサクッと作りたいときにおススメです。このお手軽さから、NTTドコモやキャディでも、積極的に活用されているようです。
- 公式サイト：https://streamlit.io/
- リポジトリ：https://github.com/streamlit/streamlit
- アップデート情報：https://docs.streamlit.io/develop/quick-reference/changelog
- APIリファレンス：https://docs.streamlit.io/develop/api-reference
- デプロイについて：https://docs.streamlit.io/deploy/streamlit-community-cloud/deploy-your-app
- NTTドコモでの活用事例：https://xtech.nikkei.com/atcl/nxt/news/24/00305/
- キャディでの活用事例：https://caddi.tech/archives/3327
🔢OR-Tools
数理最適化ライブラリには OR-Tools を採用しました。OR-Tools は、Google が開発した無料のオープンソースソフトウェアで、Python、C++、Java、C# と複数の言語をサポートしています。また、複数のソルバーを用意しており、様々な最適化タスクに対応できます。今回の数独を解くような組み合わせ最適化問題には、CP-SATソルバーが適しています。CP-SATは、制約プログラミング (Constraint Programming, CP) と満足可能性問題 (Satisfiability Problem, SAT) の略です。OR-Tools (CP-SAT) では、まず変数を用意し、その変数に制約（ルール）を与えると、CP-SATソルバーが自動的に解（制約に適合する変数）を求めてくれます。Python の数理最適化ライブラリとしては、PuLP も有名ですが、数独の求解タスクにおいては OR-Tools (CP-SAT) のほうが約7倍も高速だそうです。
- 公式サイト：https://developers.google.com/optimization/
- リポジトリ：https://github.com/google/or-tools
- CP-SATソルバーの使用例：https://developers.google.com/optimization/cp/cp_solver?hl=ja
- CP-SATのAPIリファレンス：https://or-tools.github.io/docs/pdoc/ortools/sat/python/cp_model.html
- OR-Tools (CP-SAT) vs PuLP：https://www.tech-street.jp/entry/2024/03/07/115647
💭OR-Toolsのイメージ
問題を解くフロー
OR-Tools (CP-SAT) で問題を解くフローは、以下に示した二次方程式の解を求めるフローと似ています。OR-Tools (CP-SAT)で問題を解く際も、定数を確認した後、変数を用意し、その変数に制約（ルール）を与えると、CP-SATソルバーが自動的に解（制約に適合する変数）を求めてくれます。
-
定数を確認
$$a=1, b=-2, c=1$$ -
変数を用意
$$x$$ -
変数に制約（ルール）を付与
\begin{align} 0 & = ax^2 + bx + c \\ & = x^2 - 2x + 1 \end{align} -
解の公式を用いて求解
\begin{align} x & = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}\\ & = \frac{-(-2) \pm \sqrt{(-2)^2 - 4 \times 1 \times 1}}{2 \times 1}\\ & = 1 \end{align}
ルールベースとの比較
問題をOR-Tools (ソルバー) で解くか、それともルールベースの手法で解くのかも、二次方程式の解を求めるときをイメージすると分かりやすいです。上記のように解の公式を用いる方法が、OR-Tools (ソルバー) を用いる方法と似ています。どんな二次方程式の問題でも、解の公式さえ覚えていいれば解くことができます。しかし、今回の問題の場合、わざわざ解の公式を用いなくても、以下のように因数分解しても解くことができます。複数の二次方程式の問題があったときに「この問題は因数分解して…、この問題は単純にルートをとって…」といった風に問題にあった最適な解き方を用いた方が、計算が簡単で間違いも少なそうす。このように問題ごとに別々の解き方を用意するのがルールベースの手法です。
\begin{align}
0 & = x^2 - 2x + 1 \\
& = (x-1)^2 \\
x & = 1
\end{align}
ルールベースの手法では問題に合わせた最適な解き方を選ぶことができますが、裏を返すと、問題のパターンに合わせて条件分岐して、パータンごとに解法を用意してあげる必要があります。それに対し、OR-Toolsは、変数を用意し、そこに制約を加えれば、あとはソルバーに解く作業を一任することができます。
🎲数独のルール
OR-Toolsで数独を解く前に数独のルールを説明します。数独では、最初に9x9の穴あきのテーブルが用意されます。
このテーブルの空欄を埋めていくのですが、その際、「縦一列・横一列・3x3グリッド に同じ数字が入らない」というルールを守らないければいけません。
⚠️ 縦一列の例
縦一列に同じ数字が入らないというルールがあるので、この場合青枠内の空欄には「🐵9」が入ります。
⚠️ 横一列の例
縦一列に同じ数字が入らないというルールがあるので、この場合青枠内の空欄には「🐍6」が入ります。
⚠️ 3x3グリッドの例
3x3グリッドに同じ数字が入らないというルールがあるので、この場合青枠内の空欄には「🐰4」が入ります。
以上のルールに従いながら順に空欄を埋めていき、以下のように全ての空欄を埋めることができたらゲームクリアです🎉
🔢OR-Tools で数独を解く
サンプルコードを以下の「数独ソルバー」リポジトリにまとめたので、是非参照してください。
🎲数独を解くフロー
ここでは、OR-Tools で数独を解くフローの概要を説明します。説明時の図には、@ydclab_0007さん「最適化① - ナンプレをortoolsで解いてみる」の図が非常に分かりやすかったの引用させていただきました🙏
-
定数を確認
数独の場合はテーブルに関する情報が定数になります。
- テーブルのサイズ (9x9)
- グリッドのサイズ (3x3)
- マスに入る数字の範囲 (1～9)
- テーブルの初期状態 (すでに埋まっているマスがあるため)
詳細：https://github.com/TakanariShimbo/sudoku-solver/blob/master/table.py
-
変数を用意
テーブルのサイズが 9x9 で、各セルに 1～9 の値が入るので、ブール変数の三次元配列 (9x9x9) を作成します。以下の図では、横方向が列、縦方向が行、奥行方向が数字を表しています。
詳細：https://github.com/TakanariShimbo/sudoku-solver/blob/master/variables.py
-
変数に制約（ルール）を付与
以下の5つの制約を付与します。
① 一つのセルに注目したとき、どれか一つの数字の要素が必ず選択される
② 一つの行・一つの数に注目したとき、どれか一つの列の要素が必ず選択される
③ 一つの列・一つの数に注目したとき、どれか一つの行の要素が必ず選択される
④ 一つのグリッド・一つの数に注目したとき、どれか一つのセルの要素が必ず選択される
⑤ 初期状態ですでに埋まっているセルは、その値を反映させる
詳細：https://github.com/TakanariShimbo/sudoku-solver/blob/master/constraints.py
-
CP-SATソルバーを用いて求解
これまでの手順で、変数の用意と、変数への制約の付与が完了しているので、あとは自動でCP-SATソルバーが解を求めてくれます。
詳細1：https://github.com/TakanariShimbo/sudoku-solver/blob/master/optimizer.py
詳細2：https://github.com/TakanariShimbo/sudoku-solver/blob/master/solution_callback.py
⌛解くためにかかる時間
私のPCで以下のサンプルプログラムを実行してみました。一般的なデスクトップPCを使っており、特別なスペックのPCは使っていません。その結果が以下の通りです(0は空欄)。変数を用意する際に、ブール変数の三次元配列 (9x9x9) を作成しました。場合の数を考えると $ 2^{(9 \times 9 \times 9)} = 2^{729} \approx 10^{219} $ になります。この膨大な数の中からたったの$ 0.028 s $と$ 10^{-2} $オーダーの速度で解を求めることができています。
-------- WallTime --------
0.028089 s
-------- Probrem --------
1 2 3 4 5 6 7 8 9
1 0 8 0 4 0 0 0 9 0
2 0 6 0 0 0 0 1 3 0
3 0 0 1 7 0 0 0 0 0
4 0 0 6 0 0 0 5 0 0
5 7 0 5 0 9 0 0 0 0
6 0 0 0 0 0 8 0 0 3
7 5 2 0 3 0 0 0 7 6
8 0 7 0 0 0 0 0 0 0
9 0 0 0 0 4 0 0 0 0
-------- Solution --------
1 2 3 4 5 6 7 8 9
1 2 8 3 4 5 1 6 9 7
2 4 6 7 9 8 2 1 3 5
3 9 5 1 7 3 6 8 2 4
4 8 4 6 2 7 3 5 1 9
5 7 3 5 1 9 4 2 6 8
6 1 9 2 5 6 8 7 4 3
7 5 2 8 3 1 9 4 7 6
8 3 7 4 6 2 5 9 8 1
9 6 1 9 8 4 7 3 5 2
サンプル：https://github.com/TakanariShimbo/sudoku-solver/blob/master/sample.py
リザルト：https://github.com/TakanariShimbo/sudoku-solver/blob/master/result.txt
🐧アプリでの応用例
アニマル数独アプリで、どのように数独ソルバーを応用しているかについて紹介します。
🐗回答を見る
アプリでは、「🐗回答を見る」をクリックすると問題を自動で解いてくれます。これは数独ソルバーの機能をそのまま使っています。
✅入力チェック
アプリでは、ユーザーがセルに数字を入力した際、正しいか間違っているかを自動で判定します。このとき、事前に用意した正解のテーブルと照らし合わせていません。ユーザーが入力した数値を仮反映させて、そのテーブルを解くことができるかどうかで、入力の正誤を判定しています。つまり、ユーザーの入力毎にソルバーが実行されています。ソルバーが$ 10^{-2} $オーダーの速度で解を求めることができるからこそ、これが可能となっています。
🐸問題を変える
アプリでは、「🐸問題を変える」をクリックし、空白なマスの数を設定すると自動で問題を生成します。これも、事前に用意した問題を表示しているわけではありません。全て空欄のテーブルに対してソルバーを実行することで、矛盾なく完全に埋められたテーブルを自動生成し、その完成したテーブルに対して、ユーザーが指定した数の空欄を空けることで回答を作成しています。この時、毎回同じ問題が生成されてしまわれないように、ソルバーのシード（発生する乱数）を変更するようにしています。
🙇🏻終わりに
今回のアニマル数独アプリの例から、数理最適化を活用することで、問題をパターンに分けてそれぞれの解法を用意することなく、高速に最適な解を求めることができることを実感していただけたかと思います。これまでデータドリブンなAIを業務で使用していましたが、最近数理最適化を業務で使用する中で、前者とは異なる領域の業務効率改善・DXにつながりそうだなと可能性を感じています。この記事が、数理最適化に興味を持つきっかけになれば幸いです。