« 現地時刻というか時差というか | トップページ | ナンプレ(数独)を解くAndroidアプリ »

2013年9月16日 (月)

制約ソルバーにスリザーリンクを解かせる話

最近ヒマなので(苦笑)、スリザーリンクを解くプログラムを作っていたのです。

いちおう、SlitherLinkPlayer というプログラムがあることは知っていて、相当速いことはわかっていたし、そのソースが公開されていることも知っていた。でも、まぁ、基本、プログラム作ること自体が楽しいわけで、ちょっとずつ作っていたのです。ちょっとずつ直して、やっとSlitherLinkPlayerに匹敵する性能になって来たところなのですが、そうしたら、こんなページに気づいたのですよ。

Slitherlink Solver in Copris
http://bach.istc.kobe-u.ac.jp/copris/puzzles/slitherlink/index.html

でもって、これがまた速い。私のプログラムとかSlitherLinkPlayerとかと同レベル。… という書き方だと、SlitherLinkPlayerはともかく、自分のプログラムを高性能の基準にしているみたいだけど、そういう意味じゃないのです。SlitherLinkPlayerも、私のプログラムも、「スリザーリンクを解くプログラム」として作ってあって、スリザーリンクを速く解くためにいろいろと工夫をしている。でも、上の Slitherlink Solver in Copris は、そうじゃない。

Slitherlink Solver in Copris というプログラムで、パズルの答えを探している中核部分は、SAT solver というものなのです。平たく言うと、SAT というのはブール代数(論理式)の連立方程式のことで、SAT solver というのは、その方程式を解くプログラムです。Slitherlink Solver in Copris というは、スリザーリンクの問題を、方程式に変換して、その方程式を SAT solver に解いてもらって、その方程式の解をスリリンの答えに書き直す、という仕組みでできているのです。しかも、スリザーリンクの問題を直接SATに変換するのではなくて、CSPという整数の制約問題に変換し、それを再度SATに変換し直しているのです。

※ 10x10マスのスリザーリンクの問題が、変数(未知数)が約500個、式(方程式、というか、項)が約4000個程度のSATに変換されるようです。

なんだか、はげしく回り道のような気がするし、SAT solver というのは非常に汎用的な動作をするはずなので、スリザーリンク特有のことは何も知らない。そんなので速いはずがない、なんて思っていたら大間違い。だいたい同じ性能で動作するのです。

ちょっとショックでした。

SATというのは、NP完全性みたいなことを勉強すると教科書に必ず出てきます。私は大学でそういう分野をやっていたので、当然ながらおなじみ。何か別の問題をSATに帰着させるという手法もおなじみ。それは、そうなのですが、私が勉強したときには、この手法は、ある問題が「実用的に解けない」ことを示すための手段でした。SATはNP完全なので、NPに属す問題はかならずSATに帰着できる、というのもまぁ不思議でもなんでもありませんが、実際にそうやって帰着させて、そのSATの問題を解くことによってもとの問題の解をみつける、というやりかたで、実際の問題を実用的な速度で解くことができる、というのが、なんだか超現実的な気がします。

余談

上の Slitherlink Solver in Copris のページを見て試したときに二点ほどハマりました。

  • scala は最新版をダウンロード・インストールしてはダメで、ちょっと古い version 2.9.2 を使う必要がありました。(ページには、version 2.9 と書いてありますが、2.9でなければダメ、と強調してないので、version 2.9 以降ならなんでもいいと思ってしまいハマりました。)
  • 現在(無料の SAT solver 中で)最高速らしい glucode を使う場合、「外部SAT solverを使う場合には“-s1 glucose”オプションを指定」のようなことが書いてありますが、実際には、glucose の場合も minisat の場合も、“-s1”ではなくて“-s2”にする必要がありました。また、PATHの設定が微妙なため、glucose のバイナリを cygwin1.dll と同じ c:\cygwin\bin に置いた上で、フルパスを指定して“-s2 c:\cygwin\bin\glucose_static.exe”と指定する必要がありました。

« 現地時刻というか時差というか | トップページ | ナンプレ(数独)を解くAndroidアプリ »

コメント

コメントを書く

(ウェブ上には掲載しません)

トラックバック

この記事のトラックバックURL:
http://app.f.cocolog-nifty.com/t/trackback/285638/53278597

この記事へのトラックバック一覧です: 制約ソルバーにスリザーリンクを解かせる話:

» ナンプレ(数独)を解くAndroidアプリ [Alissa Sabre at Second Life]
前の記事にも書いたとおり、SATソルバーで実用的にパズルが解けるということを知っ [続きを読む]

« 現地時刻というか時差というか | トップページ | ナンプレ(数独)を解くAndroidアプリ »