プログラミングのブログ

個人的な技術メモや制作物について書く

BDD を使った数独ソルバーが完成した

BDD に演算キャッシュを導入したり、制約を合成する順番を変えたりしたところ、ヒント数が17以上だと10~30秒ぐらいで解けるようになった。ここにある
ヒント数16のナンプレ問題が発見された - TIM Labs
ヒント数が最小の17の問題で試したところ

329|851|746
854|679|132
761|234|985
-----------
592|387|461 
643|192|578 
187|465|293 
-----------
276|918|354 
435|726|819
918|543|627 

という、答えが30秒ぐらいで出力された。作成された BDD ノードのレコードが、3,610,600個。このレコードが 3 つの int からなり12バイトなので、全体で 43,327,200 バイト = 約 43 Mバイトとなった。結構メモリは小さい。あと、Bdd レコードの重複を避けるためのハッシュマップの項数が3,610,598個で一つ16バイト なので 57,769,568バイト = 約57 M バイト。演算キャッシュの項数が7,400,479個で、一つ 14 バイトなので、103,606,706 バイト = 約 103 M バイト。
以上の合計で約 200 M バイト のメモリを使用している。プログラムは後でのせる

もしかしたら、たまたまうまくいっただけかもしれない。上記の問題から1つだけ空白に変えたところ、時間がかかりメモリも足りなくて落ちた。安定して問題を解くには、ヒント数が一定以上じゃないとだめなのか、それともマスの埋め方によっては苦手な問題があるのか。いくらか試してみないとわからない。