プログラミングのブログ

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

BDD で数独ソルバーを作るメモ3

 昨日の制約を分割する手法でうまくいったが、ならもっと制約を分割したらどうなるのか試した。そうしたら逆に遅くなった。横の制約と3×3のブロックの制約を合わせた BDD へ統合するのにちょうどいい大きさに制約を分割する必要があって、昨日がたまたまうまくいったらしい。

昨日の手法での時間を計ったら難しい問題を解くのに100秒ぐらいかかっている。時間がかかっているのは、3×3のブロックの1段目と2段目の縦の制約や2段目と3段目の縦の制約を大本の BDD に統合するところ。1段目と3段目の縦の制約は5秒ぐらいなので他よりも大分短い。

他の問題は、大体10~15秒以内に解けている。必ずしも最上級の問題が時間がかかるわけでもなく、上級の問題の方が時間がかかる場合もある。プログラムにとっての難しさと、人の難しさが違っている気がする。もう少し無駄な部分を省けば少しだけ早くなりそうだが、これ以上は数独の BDD の構造から高速にするのは無理そう。人が使う難易度の高い推論テクニックを利用しないとダメそうだが、それを使うと BDD を使う必要がなくなるのが問題になる。

[追記]
とりあえず、無駄な制約や変数を作っているところを減らしたところ、100秒かかる問題が50秒ぐらいで解けるようになった。数秒で解ける問題は1秒未満で解けるようになり結構速くなった。