数独ソルバーを書いている
android で数独のアプリを作成している。このなかに問題作成機能を作ったが、実際に作った問題の解が複数あるかどうかを高速に判定する必要があると思う。
それで、BDD で数独ソルバーを書いているがなかなか難しい。適当に考えた制約は、
(1)各マスには1つの数字が入る、複数の数値は入れられない
(2)問題として埋められているマスは、その数値を必ずとる
(3)同じ行のマスで重複した数値は入れられない
(4)同じ列のマスで重複した数値は入れられない
(5)3×3の小さい表の中では、同じ数値のマスがあってはいけない
と考えたて BDD で制約を構築していったが(1), (2) は高速に構築できたが、(3) がたぶん10分ぐらいかかりそう。(5)も結構、時間がかかりそう。(4)は試していないが同様に時間がかかると思う。
実際に実装した制約は、
- 各マスについて、問題として埋められているマスならその値を必ず取る。そのマス以外は自由な値をとるもの。例えば5で埋められているなら
(1でない and 2でない and 3でない and 4でない and 5を取る and 6でない and ... and 9でない)
- そのマスが空なら、縦横、3×3のテーブルの中で使用されていない数値をどれかとる。例えば使用されていない数値が３，４だったら
(1でない and 2でない and 3を取る and 4を取らない and ... and 9を取らない) or (1でない and 2でない and 3でない and４を取る and ... and 9でない)
のような感じで制約を作っている。
時間がかかる制約は、問題に依存しない制約なので、あらかじめ作成しといて（１）、（２）の制約と組み合わせればいいのか？あとは、android 上で動かすのでメモリの問題があるし、実行時間も。
