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

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

BDD で高速に答えを求めるは難しそうと思い始めている。縦の列の制約を作るのが時間がかかり、その制約を作らない方法で実装しようと考えている。縦の制約が難しいのは変数順序の問題だと思う。 BDD の変数順序としては、一番上の行から左へ順番にマスの番号…

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

android で数独のアプリを作成している。このなかに問題作成機能を作ったが、実際に作った問題の解が複数あるかどうかを高速に判定する必要があると思う。それで、BDD で数独ソルバーを書いているがなかなか難しい。適当に考えた制約は、(1)各マスには1つの…

クヌース先生のアルゴリズム本の4巻を読んでいる。BDD の話が載っているので簡単に Java で実装していく。 まず、BDD のノードのクラスは、 public BddNode Zero = new BddNode(0, null, null); // 終点となる 0ノードと public BddNode One = new BddNode(0…