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で効率的に解くことができるものになるみたいです。

プレゼン資料掲載しました

本日無事に、日本Androidの会横浜支部の第18回定例会で、「OpenCVとSAT4Jを使ってナンプレに挑戦してみた」と題してしゃべることができました。

参加者の皆さんから、いろいろと参考になるフィードバックもいただきました。ありがとうございました。

使ったプレゼン資料をSlideShareに載せましたので、興味のあるかたはご覧ください。

http://www.slideshare.net/AlissaSabre/opencvsat4j

メモリ管理の話の続き

先日の記事の最後の部分に書いた、Java VM がネイティブヒープも管理するという話の続き。

Javaからネイティブコードを呼び出すときにはjniという仕組みを使う。

jniでは、呼ばれる側（ネイティブコード側）が、Javaからjniで呼ばれるということを全力で意識したコーディングが必要になる。ただそれは入り口だけで、内部の処理は普通のC++（または、C++から呼べる任意の言語）のライブラリとしてコーディングすればいい。メモリ管理の仕組みも普通のC++と全く同じだ。

Sun (Oracle) のJVM用にjni用ネイティブコードを開発するときには、コンパイラとかCライブラリとかは、特にJavaを意識していない、普通のCコンパイラ、普通のCライブラリを使う。だから、メモリ管理の実装（例えばmallocの内部処理）は、JVMとは無関係なものになる。

でも、Androidの場合は、Android用のC/C++開発環境というのは、AndroidのJVM (Dalvik) から呼び出されるjniネイティブコードを作る専用の環境だ（よね?）だから、そこで提供するCライブラリは、APIは普通のCライブラリと互換でも、内部の処理が普通のCライブラリと同じである必要はないと思うのだ。例えば、malloc() という関数が、内部で Dalvik のAPI を呼んだりしても一向に構わない。

そういう仕組みにすれば、ネイティブコードが使うネイティブヒープの利用状況を、Dalvik が正確に把握することができて、ネイティブコードが malloc() を呼んだときにネイティブヒープが不足していたら malloc() がすぐにNULLを返さずに Dalvik が GC する、なんてことも可能だろうと思ったのだ。

本当にそうなっているのかどうか、Dalvik も NDKのCライブラリも、たぶんソースが公開されているんだろうから、自分で調べればわかると思うのだが、調べていない。単に妄想しているだけなのだけれども。

あと、.NET の CLR はやっている、と書いたのは、上に書いたような malloc がGCを起動する、というものとは別の仕組みだが、memory pressure のことを意識していた。

JVMに比べると、.NET の GC は、非常にたくさんの（それなりにヤヤコシくて使うのが難しい）APIを公開しているのだが、その中に memory pressure という機能がある。これは、ネイティブヒープの利用状況を、GC に教える仕組みだ。

.NET ではネイティブコードの呼び出しは P/Invoke という仕掛けで行う。これは、jniと違い、呼ばれる側（ネイティブコード側）は.NET からの呼び出しであることを一切意識せず、逆に呼び出す側（マネジドコード側）がネイティブコードの呼び出しを意識することになっている。このため普通は、jniではネイティブ側に書くいわゆるグルーコードは、P/Invoke では .NET 側で書く。

このとき、P/Invoke でネイティブコードを呼び出す直前とか戻った直後とかに、ネイティブ側で割り当てたメモリの量をGCに教えるのだ。新たに割り当てたときには AddMemoryPressure、解放したときには RemoveMemoryPressure というメソッドを呼ぶことになっている。両メッソドが適切に呼ばれていれば、CLRはネイティブメモリ利用状況を把握することができて、適当な上限値を越えるとGCを動かす、ような処理を行う、らしい。（実は、この辺り、正確な記述をみつけていないのだが。断片的な情報を組み合わせると、こんなところだと思う。）

この手法は、さきほど妄想した「ネイティブコードはmallocを呼ぶだけでOK」に比べると、余計な手間がかかるし、正確性にも劣るが、それでも、Sun JVMの「ネイティブヒープの使用量には一切関知しません。以上。」みたいなスタンスよりは大分いい。

約411年前のある日

「約411年前のある日」っていう表現はおかしいと思う。「411年」と正確にわかっているのだから「約」じゃないはず。「約400年前」なら妥当だが。

LTやります

日本Androidの会 横浜支部の定例会で、LTやらせていただくことになりました。

11月16日(土)の午後、会場はJR横浜駅から徒歩7分だそうです。

http://atnd.org/events/44595

タイトルはまだ確定できていませんが、今作っているプレゼンの最初のページには「OpenCVとSAT4Jを使ってナンプレに挑戦してみた」と書いてあります。先日Google Playで配り始めた「ナンプレ破り」の中身の話です。

面白いかどうかは、… なんとも言えませんが、あ、でも他の方の話もありますから。