トップ «前の日記(2009-02-22) 最新 次の日記(2009-02-24)» 月表示 編集

日々の流転


2009-02-23 [長年日記]

λ. Darwinで数独を解く

Paradoxで数独を解いてみたので、そのついでにDarwinでも試してみた。 Paradoxが既存のSATソルバを利用していたのに対して、DarwinはSATソルバの基本アルゴリズムであるDPLLアルゴリズムの一階述語論理版として Model Evolution Calculus というのを考えて、それを使っているとか。 ただ、実際に試してみると、Paradoxより随分時間がかかるようだ。 これは等号に直接対応していないため?

本日のツッコミ(全7件) [ツッコミを入れる]
ψ 竹内 (2009-02-28 08:56)

ParadoxとDarwin、 面白そうですね。僕は相変わらず遅いままの<br>Prologプログラムで数独作ってます。(そろそろ改良しよう...)<br>話は変わりますが4月からまたしばらく神奈川ですむことに<br>なりましたのでよろしく(^^;

ψ さかい (2009-02-28 12:35)

この手のツールは結構あるので、色々試してみると面白いと思いますよ。<br><br>> 話は変わりますが4月からまたしばらく神奈川ですむことになりましたのでよろしく(^^; <br>おお。そしたら今度みんなで集まりましょう。

ψ とおる。 (2009-02-28 13:39)

ぼくもまえに MEPHISTO の制約システムで数独ソルバーを作ってみました。一階述語論理じゃないので、限界があるんですけど。<br>http://www.nicovideo.jp/watch/sm4876059

ψ さかい (2009-03-01 13:07)

おお。やっぱり視覚化されてると、見てて楽しいですね。<br><br>> 一階述語論理じゃないので、限界があるんですけど。 <br>一階述語論理の利点は記述の容易性だと思うので、MEPHISTOでの記述が簡単なら、それは気にする必要はないかと思います。<br>非決定性(トライアンドエラー)の話でしたら、記述言語が一階述語論理かというよりも、制約解消アルゴリズムの話になるような……

ψ とおる。 (2009-03-01 15:20)

うん。でも、一階述語論理の場合は、可能な値を列挙できるようにルールを与えるものですよね?<br>逆にほかの制約解消アルゴリズムでは、たとえば、反復計算によって数値的に計算したりとか(これもある意味トライアンドエラーだけど)、そういう方が多いんじゃないかなぁとか思うんだけど、そんなことないかな?

ψ さかい (2009-03-03 01:19)

うーん。<br>ParadoxやDarwinで値の列挙が可能なのは、これらのアルゴリズムが有限のサイズのモデルしか探さないからであって、一階述語論理それ自体に理由があるわけではないです。<br>なので、一階述語論理かどうかというよりは、制約が与えられたときに、解を具体的に一つ計算するのか、それとも必要な条件がそろうまでは具体的な解は計算しないのか、というアルゴリズムの性質の問題なのかな、と。<br>どっちのタイプのアルゴリズムが多いかはちょっとわかんないですが……

ψ とおる。 (2009-03-03 13:14)

ああなるほど。一階述語論理=有限だと思い込んでました。勉強になりました。