« 2013年8月 | トップページ | 2013年10月 »

2013年9月の記事

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”と指定する必要がありました。

2013年9月11日 (水)

現地時刻というか時差というか

インターネットで遠く離れた人と会話をするには、時差が不便だ。「いつ」の話をするのがややこしい。地域によって、同じ瞬間をあらわす時刻が違うのは面倒だ。ちゃんと確認しないと間違えるし、相互に変換するのもややこしい。

Second Life には「SL標準時」というものがあって、in-world で(Second Lifeの中で)はそれを使いましょうということになっている。アイディアはいいと思うのだ。標準が一つあれば、みな、自分の現地時刻とSLの標準時との二つだけ意識して、誰とでも意思疎通ができる。でも、このSL標準時というのは失敗だと思うのだ。SL標準時が、カリフォルニア時間にペグしているのが敗因。仮想世界なのに夏時間まであって、どの瞬間にカリフォルニアが夏時間から冬時間に切り替わるかを把握していないと運用できない。

夏時間と冬時間の切り替わりのタイミングなんて、その地域に住んでいない人は知るわけが無い。というか、地元の人でもちゃんとわかってない人がおおい。切り替えが近づくと、新聞とかテレビとかで「明日から夏時間ですよ」と言うので、それにしたがっているだけ。どういうルールで切り替わるかを知らなくても、それで生活できるから。問題は、他の地域の新聞には、その情報が掲載されないことだ。

それはともかく。

グローバルなコミュニケーションというのはSecond Life特有のものではなくて、今の世の中いろいろな場面で行われていて、時刻の問題も共通。世間ではどうしているかというと、そういうときにはUTC(世界協定時)を使うのが常識。昔グリニッジ標準時と言っていたものの現代版だ。

それで、日常的に他の地域に住んでいる人と時刻の話をしていると、自分の現地時刻とUTCとの対応がなんとなくわかっちゃって、いちいち計算しなくても対応が把握できるようになるらしい。(私は、そうじゃないけれど。)

要は、日本で年を言うのに、西暦と元号と二通りあるような感覚だと思うんだよね。普段から両方をごっちゃにして使っていると両方とも普通になっちゃうという。バイリンガルみたいなセンスに近いかも。

今は、日常的にUTCを使う人というのは、限られた一部の人たちだけだけど、今後確実にそういう必要は増える。そうすると、日本に住んでる人たちが時刻の話をするときにも、日本時間じゃなくてUTCで会話なんていうことが増えたりすると思うんだよね。

今、日本では、年を言うのに西暦が普通か、元号が普通か、なんていうのはどっちが多いかよくわからないけれど、少なくとも僕は普段は西暦しか意識していない(元号を意識するのは、役所に出す書類を書くときくらいかな)し、そういう人も少なくないはず。

で、ま、そのうち、現地時刻なんて使わず、常にUTCだけ意識して生活する人が増えるんじゃないか、って思うのだ。これはもちろん、日本だけじゃなくて、全世界でね。とは言え、こういうのは習慣だから、たいてい若い世代から新しい流儀が普及して、年長者がそれにマユを潜めたり、ときには権力を使って古い流儀を強制したりして、まぁ、切り替わりには長い年月がかかったりするわけだが。

そういえば、Second Lifeも、L標準時を廃止して、UTCにするべき、と、6年くらい前に主張したのだが、変わってないよね。ま、そういうことだ。

※ 最近、私、WARFRAMEっていうゲームやってるんですけど、これは最初から時刻がUTCで設計されていて気分がいい。運営のアナウンスが「アメリカ東海岸時刻」で出るのが残念だけどね。

« 2013年8月 | トップページ | 2013年10月 »