プログラミングのブログ

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

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

 先ほどの記事で、変数順位の関係で数独の縦の制約を作るのが時間がかかり難しいと書いた。それで、縦の制約を緩めた制約を利用し、3×3のブロックの制約、横の制約と合わせた BDD を構築することにした。それを、深さ優先探索時の枝狩り手法と合わせて数独を解く。

結果から言うとうまくいった。
www.sudokugame.org
ここの問題の上級の314番を、さっきまでのコードではメモリが足りなくてだめだったが、解けるようになった。どんな制約を使ったのかを説明すると、

 -----------------------------------------
|           |             |             |
|     A     |             |             |
|           |             |             |
 -----------------------------------------
|           |             |             |
|     B     |             |             |
|           |             |             |
 -----------------------------------------
|           |             |             |
|     C     |             |             |
|           |             |             |
 -----------------------------------------

この図のように表の左端の3×3のブロック、A、B、Cとする。これをまとめて縦の列の制約にするのが難しい。そのため、AとB、BとC、AとCとそれぞれでマスの値が異なるという、全体ではなく部分的にした制約を構成することにした。つまり、A の1列目の1行目とBの1列目の全てのマスが異なる値を取る、Aの1列目の2行目とBの1列目の全てのマスが異なる、Aの1列目の3行目がBの1列目の全てのマスが異なるというという制約にした。これにより出現する変数の数と変数間の距離を少なくした。同様にBとC、AとCも制約を作った。

元の制約では1列の中のすべてのマスが異なるように制約を作っていたため、Aの列の中でもマスが異なるようにしていた。しかし、Aの列内でマスの値が異なるのは、すでに3×3のブロック内の制約で保障されているので、A内での比較を避けて結果的に無駄な変数を減らすことができた。AとCの制約を作るのは難しいかと思ったが10~20秒ぐらいで作成できた。こうやって作った制約のBDD を使用し、深さ優先探索で問題を解いたところ早く問題を解くことができた。

この制約自体は、固有の問題と関係がなく事前に作っておけば高速に問題を解くことができそうに思える。そこら辺を整理して、制約を作る際の時間がかかる部分を準備したい。

[追記]
こうやって作った縦の制約が元の制約と同じだわ。なので、深さ優先探索をしなくても問題が解けた。