2009-02-23 [長年日記]
λ. Darwinで数独を解く
Paradoxで数独を解いてみたので、そのついでにDarwinでも試してみた。 Paradoxが既存のSATソルバを利用していたのに対して、DarwinはSATソルバの基本アルゴリズムであるDPLLアルゴリズムの一階述語論理版として Model Evolution Calculus というのを考えて、それを使っているとか。 ただ、実際に試してみると、Paradoxより随分時間がかかるようだ。 これは等号に直接対応していないため?
- 入力ファイル sudoku-darwin.tptp
- ログ sudoku-darwin.txt
ParadoxとDarwin、 面白そうですね。僕は相変わらず遅いままの<br>Prologプログラムで数独作ってます。(そろそろ改良しよう...)<br>話は変わりますが4月からまたしばらく神奈川ですむことに<br>なりましたのでよろしく(^^;
この手のツールは結構あるので、色々試してみると面白いと思いますよ。<br><br>> 話は変わりますが4月からまたしばらく神奈川ですむことになりましたのでよろしく(^^; <br>おお。そしたら今度みんなで集まりましょう。
ぼくもまえに MEPHISTO の制約システムで数独ソルバーを作ってみました。一階述語論理じゃないので、限界があるんですけど。<br>http://www.nicovideo.jp/watch/sm4876059
おお。やっぱり視覚化されてると、見てて楽しいですね。<br><br>> 一階述語論理じゃないので、限界があるんですけど。 <br>一階述語論理の利点は記述の容易性だと思うので、MEPHISTOでの記述が簡単なら、それは気にする必要はないかと思います。<br>非決定性(トライアンドエラー)の話でしたら、記述言語が一階述語論理かというよりも、制約解消アルゴリズムの話になるような……
うん。でも、一階述語論理の場合は、可能な値を列挙できるようにルールを与えるものですよね？<br>逆にほかの制約解消アルゴリズムでは、たとえば、反復計算によって数値的に計算したりとか（これもある意味トライアンドエラーだけど）、そういう方が多いんじゃないかなぁとか思うんだけど、そんなことないかな？
うーん。<br>ParadoxやDarwinで値の列挙が可能なのは、これらのアルゴリズムが有限のサイズのモデルしか探さないからであって、一階述語論理それ自体に理由があるわけではないです。<br>なので、一階述語論理かどうかというよりは、制約が与えられたときに、解を具体的に一つ計算するのか、それとも必要な条件がそろうまでは具体的な解は計算しないのか、というアルゴリズムの性質の問題なのかな、と。<br>どっちのタイプのアルゴリズムが多いかはちょっとわかんないですが……
ああなるほど。一階述語論理＝有限だと思い込んでました。勉強になりました。