BDD で数独ソルバーを作るメモ１ - プログラミングのブログ

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

BDD の変数順序としては、一番上の行から左へ順番にマスの番号 n を付けている。そして、そのマスが 1 になる、２になる、…　9になるときに1枝を取る変数が9個存在する。つまり、マス１には、x_1~x_9 までの変数が対応し、マス n には、x_{(n - 1) × 9 + 1} から x_(n × 9) の変数が対応する。(n-1) × 9 は、そのマスの前までにある変数の個数を表している。

このように、変数を付けていると縦の列で同じ数字が表れないという数独の制約を作る際に、その制約にある変数が飛び飛びの変数を取る。そのため、BDD の共有化が行われにくくなる。例えば、1列目の制約は

{(x_1 == 1) and (x_82 == 0) and (x_163 == 0) and ... and (x_657 == 0)} or

{(x_2 == 1) and (x_83 == 0) and (x_164 == 0) and ... and (x_658 == 0)} or

…

{(x_9 == 1) and (x_90 == 0) and (x_171 == 0) and ... and (x_665 == 0)}
という制約になり、同じ変数が現れずノードの共有化が起きそうにない。さらに2列目、3列目と同じ変数が表れない制約を追加していくのでどんどん膨らむと思う。

この制約を作るのが難しいので、少し緩めた制約を作って BDD と組み合わせていき BDD のサイズを小さく保つようにしようと考えている。また、他には、横の制約と小さい3×3のブロックの制約のみを満たした BDD を作成し、深さ優先探索の枝狩りに利用する方法を考えた。後者の方をさっそく実装したが、ある問題で試したところ演算キャッシュのメモリが足りなくて途中で落ちる。コードを乗せると、

private int ans_bdd = store.getZeroNode(); // 見つかった答えを保存する bdd
	
private void createAnsBdd(int row, int colmn, int bdd_node, boolean[][] usedDigit) {
	if(bdd_node == store.getZeroNode()) // bdd_node が空になったら答えがない
		return ;
	if(row == -1) {
		if(bdd_node != store.getZeroNode()) {
			// 答えを見つけたら保存しておく
			ans_bdd = store.or(bdd_node, ans_bdd);
		}
		return ;
	}
		
	if(table[row][colmn] != 0) { // 表が埋まっているならそれを使用する
		int variableLevel = (getCellNumber(row, colmn) - 1) * 9 + table[row][colmn];
		int node = store.getPositive(variableLevel); // x_varLevel を使用するノードを作る

		usedDigit[colmn][table[row][colmn]] = true; // 使用した数を保存する
                // ノードを組み合わせて次のマスへ行く
		createAnsBdd(colmn == 0 ? row - 1 : row, colmn == 0 ? 8 : colmn - 1, 
					store.and(bdd_node, node), usedDigit);
		usedDigit[colmn][table[row][colmn]] = false;
	}else {
		for(int digit = 1; digit <= 9; ++digit) {
                        // 現在のマスを 1~9 の数で試す
			int variableLevel = (getCellNumber(row, colmn) - 1) * 9 + digit;
                        // そのマスで選択可能で、digit が使用済みでなく、
                        // 表の縦横,3×３のブロックで矛盾しないなら digit を試す
			if(usableDigit[row][colmn][digit] && (!usedDigit[colmn][digit]) 
					&& isUsableDigitInTable(row, colmn, digit)) {
				int node = store.getPositive(variableLevel);
				usedDigit[colmn][digit] = true; // digit を使用済みにする
				table[row][colmn] = digit;
				createAnsBdd(colmn == 0 ? row - 1 : row, colmn == 0 ? 8 : colmn - 1,
						store.and(bdd_node, node), usedDigit);
				table[row][colmn] = 0;
				usedDigit[colmn][digit] = false;
			}
		}
	}
}

となる。引数の bdd_node では初め、横と3×3ブロックの制約を満たすものの数独の表をすべて持っている。そのため、深さ優先探索では横の制約を満たすようにマスに入る数を探している。そのために、usedDigit[colmn][digit] を利用している。列 colmn で使用した数をチェックしている。関数の再帰の仕方としては、右下の8行8マスの変数順位が一番高いものから、0行0マスのマスへ遷移しているため、row == -1 のときすべてのマスが探索されたことを示している。再帰呼び出しのところで3項演算子を使っているのは0列目の時に次の行へ移るため。あと、関数の呼び出しは createAnsBdd(8, 8, root_node, usedDigit); となり、8行8列目からスタートする。これにより、変数順位が一番高いものから試していくことができ、bdd 演算が早くなると思う。

しかし、これでもダメなので、縦の制約を3行分に分割した緩い制約を使用し、bdd_node を小さく枝狩りしてから深さ優先探索を行おうと考えている。正直、論文を見て、数独の推論手法を利用したアルゴリズムが高速に問題を解いていて BDD を利用したアルゴリズムをやる意味はあるのかと考えている。他にも湊先生の論文とか見ると高速に BDD で制約を作成しているので、自分の実装技術がやばそう。とはいえ、あくまで BDD を利用して高速に解くというのが目的なのでいいかなと思う。