TIM Labs

SATソルバーで25x25のナンプレが解けるだろうか

| コメント(0) | トラックバック(0)
ナンプレ(あるいはSUDOKU)というパズルをご存知だろうか。
通常は、9x9の問題なのだが、つい、25x25の問題を作った者がいる。
問題に最初から示されている数のことをヒントと言い、その個数をヒント数と言うのだが、以下がヒント数146(現在世界最少)の問題である。

+--------------+--------------+--------------+--------------+--------------+
| . 12  .  .  .| .  .  .  .  .| .  .  .  9  .| .  . 15  .  .|22  .  .  .  .|
| .  .  .  .  .| .  9  . 19  .| .  . 10 11  .| .  .  .  .  .| .  .  .  .  .|
| .  4  . 22  .| .  .  .  .  .| .  .  .  .  .| .  . 12  .  .|20 15  1  .  .|
|16  1 20 15  .| .  .  .  .  .| .  .  .  .  .|14  .  4  . 22|12 25  .  .  .|
| .  .  .  .  .| .  7  2 11  .|23  . 19  8  .| .  .  . 13  .| .  .  .  .  .|
+--------------+--------------+--------------+--------------+--------------+
|13  .  8  .  2| .  .  .  .  .| .  .  7 23  6| .  9  . 19 11| .  .  .  .  .|
| .  .  .  . 23| .  .  .  . 16| .  .  .  .  .| .  .  .  .  .| 1  .  .  .  .|
| 7  .  .  . 10| 3  .  .  .  .| .  .  9 19  .| . 13  . 23  .| .  .  .  5  .|
| .  .  .  .  .|15  .  .  . 22| .  .  .  .  .| .  .  .  .  .|25 20  .  .  .|
| .  .  .  .  .|12  . 14  1 25| .  .  .  .  .| .  .  3  .  .|16  4 15  .  .|
+--------------+--------------+--------------+--------------+--------------+
| .  .  .  .  .| . 19  9  .  .| .  . 13  7  .| .  .  .  5  .| .  .  . 23 10|
| . 22  . 25 17| .  .  .  .  .| .  .  .  .  .|12  . 20  .  .| .  .  .  .  .|
| . 20 12 16  .| .  .  .  .  .| .  .  .  . 14|15 22  1  . 25| .  .  .  .  .|
| . 15  .  .  .| . 11  .  .  .| .  .  .  .  .| .  . 16  .  .| .  .  .  9  .|
| .  .  .  1  .| . 10  . 23  .| .  .  .  . 18| .  .  .  .  .| .  .  .  .  8|
+--------------+--------------+--------------+--------------+--------------+
|10  .  .  .  8| . 13  .  5  .| .  .  .  .  .| . 19  . 11 23| .  .  .  6  .|
| .  .  . 17  7| .  .  .  .  .| .  .  .  .  1| .  .  .  .  .| 4 22  .  .  .|
| .  .  .  . 11| . 23  .  .  .| .  .  .  . 20| .  .  .  2  .|14  .  .  .  .|
|19  . 23  .  5| .  8  .  9  .| . 21  .  .  .| . 10  .  7  .| .  .  .  .  .|
| .  3  .  .  .| .  .  .  .  .|25  4  .  . 12| .  .  .  .  .|15  1 16  .  .|
+--------------+--------------+--------------+--------------+--------------+
| .  .  .  .  .| .  .  .  . 15| . 12  .  . 25| 1  . 22  .  .| 3  .  .  .  .|
|23  .  .  . 19| .  2  .  .  .| .  .  .  .  .| .  .  . 10  .| .  .  .  7 11|
| .  .  . 18  .| .  .  .  .  .| . 20  .  .  .| .  .  .  .  .| .  .  .  .  .|
| .  .  .  .  .| .  .  .  .  4|14 15  .  . 22| .  .  .  .  .| .  .  . 10  .|
|11  .  .  .  9| .  .  .  .  .| .  .  .  .  .| .  .  .  .  .| .  .  . 19  .|
+--------------+--------------+--------------+--------------+--------------+
ナンプレの問題を解くプログラムはネット上にゴロゴロ転がっているのだが、大きいサイズに対応したソルバーはなかなか存在しない。
 小さいときには、手筋を実装せず、単に再帰だけでも十分高速に解けるのだが、それではサイズが大きくなると直ぐに破綻するはずだ。

この問題、なかなか解いてくれる人がいない。
ナンプレに限らないのだが、パズルの多くは、限られたルールとヒントから解くのである。
そして、こういう問題のことを、制約充足問題と言う。
日本語での説明は貧弱なので、ぜひ Constraint satisfaction problem を参照されたい。

さて、制約充足問題というと、すぐに思いつくのがSATであろう。
ということで調べると、SATでパズルを解く研究をしている神戸大学情報基盤センターが直ぐに見つかる。

ということで、上の25x25の問題を送ってみた。さて、どうなるだろうか?

トラックバック(0)

トラックバックURL: http://labs.timedia.co.jp/mt/mt-tb.cgi/652

コメントする

このブログ記事について

このページは、fujiが2017年7月 1日 00:00に書いたブログ記事です。

ひとつ前のブログ記事は「データ解析のための統計モデリング入門 マルコフ連鎖モンテカルロ(MCMC)法とベイズ統計モデル 読書メモ4」です。

次のブログ記事は「SATソルバーで25x25のナンプレがたった20秒で解かれてしまった」です。

最近のコンテンツはインデックスページで見られます。過去に書かれたものはアーカイブのページで見られます。