数独自動ソルバのしくみ

はじめに

数独というパズルがあります。まあこんな感じのものです。

 

数独の例(画像はwikipediaより) https://ja.wikipedia.org/wiki/%E3%83%95%E3%82%A1%E3%82%A4%E3%83%AB:Sudoku-by-L2G-20050714.svg


これをコンピュータに自動で解かせるにはどうすればいいでしょうか?

 

答えは†線形計画法†です。

アルゴリズム

$729=9^3$変数の線形計画法をします。具体的には

$$0\leq x_{i,j,k}\leq 1,(1\leq i,j,k\leq 9$$

です。これらの変数は、$(i,j)$マスが$k$なら1になって、そうでないならば0とします。

 

そして、1つのマスに1つの数字しかないので$\sum_{k} x_{i,j,k}\leq 1$です。すべてのi,jについて同じようなことをするので、条件式が$9^2=81$個あります

同じ行に同じ数字は2個以上ないので、$\sum_{j} x_{i,j,k}\leq 1$です。同上で条件式81個追加です。

同じ列に同じ数字は2個以上ないので、$\sum_{i} x_{i,j,k}\leq 1$です。同上で条件式81個追加です。

また、3x3のマスに同じ数字が2個以上ないので、

すべての$a,b\in\{1,4,7\},1\leq k\leq 9$について、$\sum_{i=0}^{2}\sum_{j=0}^{2}x_{i+a,j+b,k}\leq 9$

です。条件式81個追加

 

以上、条件式はすべて合わせると$81\times 4=324$個あります。

この条件のもとで、$\sum_{i,j,k}x_{i,j,k}$を最大化せよ。

という線形計画問題を解けばOKです。

 

追記

変数の範囲は、(i,j)マスがkであることが確定するならば$x_{i,j,k}=1$であり、特にそのような条件がないならば$0\leq x_{i,j,k}\leq 1$と設定します

 

pythonには線形計画問題を解いてくれるライブラリがあるので、それに丸投げします。

入力のフォーマットとしては、空欄の場所には代わりに0を入れてスペース区切りにすればOKです。

gist.github.com

 

inputの例

5 3 0 0 7 0 0 0 0
6 0 0 1 9 5 0 0 0
0 9 8 0 0 0 0 6 0
8 0 0 0 6 0 0 0 3
4 0 0 8 0 3 0 0 1
7 0 0 0 2 0 0 0 6
0 6 0 0 0 0 2 8 0
0 0 0 4 1 9 0 0 5
0 0 0 0 8 0 0 7 9

 

冒頭で紹介した数独の問題を投げると一瞬で答えを返してくれます。

 

プログラムの3行目をK=5にすれば25x25の数独にも対応してくれます。

ネットで適当に拾った問題を試しに入力したら7秒程度で答えが出力されました。

注意点

解が複数あるときにバグりそうです

余談

プログラムを大規模に書き換える必要がありますが、他の大抵の変わり種のナンバープレース線形計画法で殴れると思います。ただ立式が大変そうです

例えば、「$(i_1,j_1)$マスより$(i_2,j_2)$マスのほうが大きい」という条件を付け足したいなら

$$x_{i_1,j_1,k_1}+x_{i_2,j_2,k_2}\leq 0$$

を、すべての$(k_1\lt k_2)$に対して追加すればOKです。$N\times N$のナンプレならば条件を$\dfrac{N(N-1)}{2}$個追加することになります。

他にも、

「$(i_1,j_1)$マスの数字と$(i_2,j_2)$マスの数字は連続してる」

や、

「$(i_1,j_1)$マスの数字と$(i_2,j_2)$マスの数字は等しい」

や、

「$(i_1,j_1)$マスの数字と$(i_2,j_2)$マスの数字の和はxだ」

も同様にいくつかの条件を追加することで達成できると思います。

このプログラムにそこまでの価値があるのかはわかりませんが、勝手に使ったり改変したりして、どうぞ

懸賞問題でズルするのに使えそうですが、知りません。

最後に

この記事は「毎月1記事更新しよう」という目的をギリギリ達成させるために月末にやっつけで書かれています。

この記事ではscipyの線形計画法ライブラリを使っていますが、pulpを使っている先行研究を見つけたのでそれを見たほうがいいです。なんならpulpを使ったほうがコードを直感的に書けるので良さそうです。