« プレゼン資料掲載しました | トップページ | USB 3.0 のUSBメモリ »

2013年11月17日 (日)

SAT Solverでナンプレを解くのにかかる時間

昨日、「ナンプレを解くのにかかる時間」についての質問をいただいた。質問者の意図を正確に把握できているかどうかわからないが、私はこの問いを「大抵の問題が2~3秒で解けるのはわかったが、とても難しい問題のときに、最大どれくらいの時間がかかるのか」という問いかけだと受け取った。

そこで昨日は、以下のようなことを答えとしてお話した。

  • 実は、よくわからない。
  • それなりにいろいろな問題を試しているつもりだが、どの問題も3秒程度で解けている。早く解ける問題はたまにあるが、特に長い時間がかかる問題は経験していない。だから、たぶん、全ての問題が3秒以内で解けるのではないかという気がしている。
  • 人間がパズルとしてナンプレで解くときの問題の難しさと、それをSATに変換してSAT Solverが解くときの難しさは、同じではないようだ。開発の初期のころに、(あまり多くない問題を)SAT4Jで解くのにかかる時間を測定しながら評価していたのだが、ナンプレ本が示す問題の難易度と、SAT Solverで消費した時間とが、逆転する(つまり、難易度が高い問題の方が短い時間で解ける)ことがあった。
  • どういうときにSAT Solverで解くのに時間がかかるのか、私にはよくわかっていないので、最悪でどれくらい時間がかかるのかも、私にはわからない。ひょっとすると、SAT Solverに向かないナンプレの問題というものがあって、それを「ナンプレ破り」で解こうとすると、いつまで待っても解き終わらずに固まってしまう(ANR)ことがあるかもしれない。そう思うと怖い。

この件について昨夜帰宅途中でいろいろと考えたのだが、まず、SAT Solverで解きにくいSAT問題について調べるべきだと思い、ぐぐってみたところ、こんな記事を発見した。

http://d.hatena.ne.jp/hzkr/20090209

この記事自体は、「ランダム生成したSATの問題が解を持つ確率」について検討し、「式(項)の個数 / 変数の個数」という値が4.27の辺りだけ、解を持つかどうかが予測できなくなる、という事実を紹介しているのだが、最後の方にこんなことも書いてある。

4.27付近は(中略)SATを解くアルゴリズムにとってとても難しいゾーンということになります。(中略)ヒューリスティックを駆使して効率的にSATを解くアルゴリズムは、式長/変数数比がこのゾーンの外ならとても効率的にSATを解けるらしいです。この4.27ゾーンだけが鬼門。

4.27ゾーンというのは、具体的には 3.5 ~ 5 くらいの範囲らしい。

ほほう、と思って、ナンプレの問題からできるSATの問題について、この比を計算してみると、11745 ÷ 729 ≒ 16.1 。めっちゃ大きい! どうも、ナンプレを変換したSATの問題というのは、大抵、SAT Solverで効率的に解くことができるものになるみたいです。

« プレゼン資料掲載しました | トップページ | USB 3.0 のUSBメモリ »

コメント

コメントを書く

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

トラックバック

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

この記事へのトラックバック一覧です: SAT Solverでナンプレを解くのにかかる時間:

« プレゼン資料掲載しました | トップページ | USB 3.0 のUSBメモリ »