BDD で数独ソルバーを作るメモ３
昨日の制約を分割する手法でうまくいったが、ならもっと制約を分割したらどうなるのか試した。そうしたら逆に遅くなった。横の制約と3×3のブロックの制約を合わせた BDD へ統合するのにちょうどいい大きさに制約を分割する必要があって、昨日がたまたまうまくいったらしい。
昨日の手法での時間を計ったら難しい問題を解くのに100秒ぐらいかかっている。時間がかかっているのは、3×3のブロックの1段目と2段目の縦の制約や2段目と3段目の縦の制約を大本の BDD に統合するところ。1段目と3段目の縦の制約は5秒ぐらいなので他よりも大分短い。
他の問題は、大体10～15秒以内に解けている。必ずしも最上級の問題が時間がかかるわけでもなく、上級の問題の方が時間がかかる場合もある。プログラムにとっての難しさと、人の難しさが違っている気がする。もう少し無駄な部分を省けば少しだけ早くなりそうだが、これ以上は数独の BDD の構造から高速にするのは無理そう。人が使う難易度の高い推論テクニックを利用しないとダメそうだが、それを使うと BDD を使う必要がなくなるのが問題になる。
[追記]
とりあえず、無駄な制約や変数を作っているところを減らしたところ、100秒かかる問題が50秒ぐらいで解けるようになった。数秒で解ける問題は1秒未満で解けるようになり結構速くなった。
BDD で数独ソルバーを作るメモ２
先ほどの記事で、変数順位の関係で数独の縦の制約を作るのが時間がかかり難しいと書いた。それで、縦の制約を緩めた制約を利用し、3×3のブロックの制約、横の制約と合わせた BDD を構築することにした。それを、深さ優先探索時の枝狩り手法と合わせて数独を解く。
結果から言うとうまくいった。
www.sudokugame.org
ここの問題の上級の314番を、さっきまでのコードではメモリが足りなくてだめだったが、解けるようになった。どんな制約を使ったのかを説明すると、
----------------------------------------- | | | | | A | | | | | | | ----------------------------------------- | | | | | B | | | | | | | ----------------------------------------- | | | | | C | | | | | | | -----------------------------------------
この図のように表の左端の3×3のブロック、A、Ｂ、Ｃとする。これをまとめて縦の列の制約にするのが難しい。そのため、AとＢ、ＢとＣ、ＡとＣとそれぞれでマスの値が異なるという、全体ではなく部分的にした制約を構成することにした。つまり、A の１列目の1行目とＢの1列目の全てのマスが異なる値を取る、Ａの１列目の2行目とＢの1列目の全てのマスが異なる、Ａの1列目の3行目がＢの1列目の全てのマスが異なるというという制約にした。これにより出現する変数の数と変数間の距離を少なくした。同様にＢとＣ、ＡとＣも制約を作った。
元の制約では1列の中のすべてのマスが異なるように制約を作っていたため、Ａの列の中でもマスが異なるようにしていた。しかし、Ａの列内でマスの値が異なるのは、すでに3×3のブロック内の制約で保障されているので、Ａ内での比較を避けて結果的に無駄な変数を減らすことができた。ＡとＣの制約を作るのは難しいかと思ったが10～20秒ぐらいで作成できた。こうやって作った制約のBDD を使用し、深さ優先探索で問題を解いたところ早く問題を解くことができた。
この制約自体は、固有の問題と関係がなく事前に作っておけば高速に問題を解くことができそうに思える。そこら辺を整理して、制約を作る際の時間がかかる部分を準備したい。
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 を利用して高速に解くというのが目的なのでいいかなと思う。
BDD を使った数独ソルバーが完成した
BDD に演算キャッシュを導入したり、制約を合成する順番を変えたりしたところ、ヒント数が17以上だと10~30秒ぐらいで解けるようになった。ここにある
ヒント数16のナンプレ問題が発見された - TIM Labs
ヒント数が最小の17の問題で試したところ
329|851|746 854|679|132 761|234|985 ----------- 592|387|461 643|192|578 187|465|293 ----------- 276|918|354 435|726|819 918|543|627
という、答えが30秒ぐらいで出力された。作成された BDD ノードのレコードが、3,610,600個。このレコードが 3 つの int からなり12バイトなので、全体で 43,327,200 バイト = 約 43 Mバイトとなった。結構メモリは小さい。あと、Bdd レコードの重複を避けるためのハッシュマップの項数が3,610,598個で一つ16バイト なので 57,769,568バイト = 約57 M バイト。演算キャッシュの項数が7,400,479個で、一つ 14 バイトなので、103,606,706 バイト = 約 103 M バイト。
以上の合計で約 200 M バイト のメモリを使用している。プログラムは後でのせる
もしかしたら、たまたまうまくいっただけかもしれない。上記の問題から1つだけ空白に変えたところ、時間がかかりメモリも足りなくて落ちた。安定して問題を解くには、ヒント数が一定以上じゃないとだめなのか、それともマスの埋め方によっては苦手な問題があるのか。いくらか試してみないとわからない。
数独ソルバーを書いている
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 上で動かすのでメモリの問題があるし、実行時間も。
真理値表からの BDD の構築
クヌース先生のアルゴリズム本の4巻を読んでいる。BDD の話が載っているので簡単に Java で実装していく。
まず、BDD のノードのクラスは、
public BddNode Zero = new BddNode(0, null, null); // 終点となる 0ノードと public BddNode One = new BddNode(0, null, null); // 1ノード public class BddNode{ private int level = 0; // 変数レベル private BddNode left, right; // 0-枝、1-枝 public BddNode(int num,BddNode lhs, BddNode rhs) { level = num; left = lhs; right = rhs; } public boolean isZeroNode() { return this == Zero; } public boolean isOneNode() { return this == One; } public BddNode getLeftNode() { return right; } public BddNode getRightNode() { return left; } public int getLevel() { return level; } public String getString() { if(this == Zero) return new String("0"); else if(this == One) return new String("1"); return new String("(" + Integer.toString(level) + "| " + left.getString() + ", " + right.getString() + ")"); } public boolean equals(BddNode node) { if(level == node.level && left == node.left && right == node.right ) return true; return false; } }
真理値表は、00010111 のような形をしている。この場合は、変数がx1,x2,x3 あり、先頭から (x1, x2, x3) = (0, 0, 0) の時の真理値、(0, 0, 1) の時の真理値、(0, 1, 0) の時の真理値 ...、(1, 1, 1)の時の真理値となる。つまり、x1, x2, x3 のすべての真理値の組み合わせ2^3 = 8 通りに対応した2進列になっている。
真理値表 00010111 を半分に分割すると、 0001, 0111 となり、前半が x1 が０の時、後半が x1 が１の時の真理値表になる。そして、半分に分割していった真理値表が BDD のノードに対応している。ということで、真理値表を再帰で半分に分割しながら、BDD を組み立てるアルゴリズムがこちら。
Vector< Vector<BddNode> > nodeStore = new Vector<>(); // 作成済みの BDD のノードを変数レベルごとに保存 public void init() { nodeStore.add(new Vector<>()); } // 真理値表の長さから現在の変数レベルを求める public int getVariableLevel(int boolTableLength) { int cnt = 0; while(boolTableLength > 0) { ++cnt; boolTableLength /= 2; } return cnt-1; } // 作成済みのノードから同じものを検索する public BddNode search(BddNode node) { if(nodeStore.size() <= node.getLevel()) return null; Vector<BddNode> sameLevelNodes = nodeStore.elementAt(node.level); for(int i = 0; i < sameLevelNodes.size(); ++i) { if(node.equals(sameLevelNodes.elementAt(i))) return sameLevelNodes.elementAt(i); } return null; // なかったら null を返す } // 作成した重複のないノードを保存する public void register(BddNode node) { while(node.getLevel() >= nodeStore.size()) { nodeStore.add(new Vector<>()); } nodeStore.elementAt(node.getLevel()).addElement(node); } // 再帰して BDD の下のノードから作成し、統合していく public BddNode createBddFromBooleanTable(int front, int back, String boolTable) { // 真理値表の長さが 1 のとき、その真理値に対応した 0ノード、1ノードを返す if(back-front == 1) { if(boolTable.charAt(front) =='0') return Zero; else if(boolTable.charAt(front)=='1') return One; } // 現在の変数レベルが０の時、真理値表の左半分に対応するので、 int mid = (back - front) / 2; // 0枝の先に左半分のノード BddNode retBddLeft = createBddFromBooleanTable(front, front + mid, boolTable); // 現在の変数レベルが１の時、右半分に対応し1枝の先のノード BddNode retBddRight = createBddFromBooleanTable(front + mid, back, boolTable); // 両方とも0ノード、もしくは、1ノードのとき対応する０ノード、1ノードを返す if(retBddLeft.isZeroNode() && retBddRight.isZeroNode()) return Zero; if(retBddLeft.isOneNode() && retBddRight.isOneNode()) return One; // 現在のノードを作り、 BddNode currentNode = new BddNode(getVariableLevel(back-front), retBddLeft, retBddRight); // 重複がないか検索する BddNode sameNode = search(currentNode); if(sameNode == null) { // 重複がないなら登録し、そのノードを返す register(currentNode); return currentNode; } // 同じのがあったら、それを返す return sameNode; }
もっと簡単にできると思ったら、ノードの重複を調べる処理で以外に長くなった。しかし、ただ単純にボトムアップに組み立てるなら、別に再帰する必要はない。再帰関数が書きたくなったから、上のように書いたけど。普通にボトムアップに組み立てるのが以下のコード。
public BddNode searchIn(BddNode node, BddNode[] nodes, int lastIndex) { for(int i=0; i < lastIndex; ++i) { if(node.equals(nodes[i])) return nodes[i]; } return null; } public BddNode createBddBottomUp(String boolTable) { // 初めに、真理値表の0,1に対応したノードを prevNode に入れておく。 // これをprevNode[i], prevNode[i+1] を組み合わせて次のレベルのノードをボトムアップに作っていく BddNode[] prevNodes = new BddNode[boolTable.length()]; for(int i = 0; i < boolTable.length(); ++i) { if(boolTable.charAt(i) == '0') { prevNodes[i] = Zero; }else prevNodes[i] = One; } int varLevel = 0; for(int i=2; i <= boolTable.length(); i *= 2) { // 2つずつ組み合わせるので半分に減っていく BddNode[] nextNodes = new BddNode[boolTable.length() / i]; // 次のノードは現在のノードの半分 ++varLevel; for(int j=0; j < prevNodes.length; j += 2) { // 二つのノードを組み合わせて次のノードを作る if(prevNodes[j] == Zero && prevNodes[j + 1] == Zero) nextNodes[j / 2] = Zero; else if(prevNodes[j] == One && prevNodes[j + 1] == One) nextNodes[j / 2] = One; else { nextNodes[j / 2] = new BddNode(varLevel, prevNodes[j], prevNodes[j + 1]); // 重複を調べる BddNode retNode = searchIn(nextNodes[j / 2], nextNodes, j / 2); // 重複があったら、そのノードをセットする nextNodes[j / 2] = (retNode != null ? retNode : nextNodes[j / 2]); } } prevNodes = nextNodes; } return prevNodes[prevNodes.length-1]; // 最後のノードが全体の BDD }
こっちの方がシンプルになる。BDD を構成する関数を描いたが、何がBDDでできるかが問題
あるViewが他のViewを再描画する
fragment にカスタム View を配置し、もう一つの fragment にその View を操作する カスタム View を配置した。
しかし、片方の View の中を invalidate() で再描画しても全体の View は再描画されなかった。
アプリ全体を再描画するものだと思っていたけど、違ったらしい。
MainActivity の layout はこうなっている。
<?xml version="1.0" encoding="utf-8"?>
<android.support.constraint.ConstraintLayout
xmlns:android="http://schemas.android.com/apk/res/android" android:layout_width="match_parent"
android:layout_height="match_parent">
<LinearLayout
android:id="@+id/linearLayout"
android:layout_width="match_parent"
android:layout_height="match_parent"
android:orientation="vertical"
android:weightSum="4"></LinearLayout>
</android.support.constraint.ConstraintLayout>ここに、MainActivity から、２つの Fragment (BeChangeFragment, operateFragment) を LinearLayout に追加している。
うちの環境では、こうやって動的に追加しないとなぜかアプリが落ちる。
public class MainActivity extends AppCompatActivity { @Override protected void onCreate(Bundle savedInstanceState) { super.onCreate(savedInstanceState); setContentView(R.layout.activity_main); if(savedInstanceState == null){ FragmentManager manager = getSupportFragmentManager(); FragmentTransaction transaction = manager.beginTransaction(); transaction.replace(R.id.linearLayout, new BeChangeFragment()); transaction.add(R.id.linearLayout, new OperateFragment()); transaction.commit(); } setColors(); } }
この BeChangeFragment の View の内容が operateFragment の View を操作したときに変更されるので、
operateFragment の View を操作したときに、BeChangeFragment の View を再描画する必要がある。
Fragment の Layout は、
<?xml version="1.0" encoding="utf-8"?>
<FrameLayout xmlns:android="http://schemas.android.com/apk/res/android"
xmlns:app="http://schemas.android.com/apk/res-auto"
xmlns:tools="http://schemas.android.com/tools"
android:id="@+id/linearLayout2"
android:layout_width="match_parent"
android:layout_height="match_parent"
android:layout_weight="1">
<com.example.name.FragmentTest.BeChangeFragmentView
android:id="@+id/be_change_fragment_view"
android:layout_width="match_parent"
android:layout_height="match_parent" />
</FrameLayout><?xml version="1.0" encoding="utf-8"?>
<FrameLayout xmlns:android="http://schemas.android.com/apk/res/android"
xmlns:app="http://schemas.android.com/apk/res-auto"
xmlns:tools="http://schemas.android.com/tools"
android:id="@+id/linearLayout2"
android:layout_width="match_parent"
android:layout_height="match_parent"
android:layout_weight="1">
<com.example.name.FragmentTest.OperateFragmentView
android:id="@+id/operate_fragment_view"
android:layout_width="match_parent"
android:layout_height="match_parent" />
</FrameLayout>となっており、それぞれカスタム View の BeChangeFragmentView, OperateFragmentView を
取り込んでいる。二つの View (それを含む Fragment も) MainActivity の layout の中で同じ ViewGroup の
LinearLayout に属しているので、そこから、BeChangeFragmentView を取り出し invalidate() を呼び出し
再描画している。上記の操作をするためには、
public class OperateFragmentView extends View { @Override public boolean onTouchEvent(MotionEvent event){ switch(event.getAction()){ case MotionEvent.ACTION_DOWN: // lisner かなんかで変更をBeChangeFragmentView に伝える break; case MotionEvent.ACTION_UP: // lisner かなんかで変更をBeChangeFragmentView に伝える break; } invalidate(); // 自分の View の再描画 getRootView().findViewById(R.id.be_change_fragment_view).invalidate(); // BeChangeFragmentView の再描画 return true; } }
と、ラストの方で、getRootView()で自分の属する ViewGroup を取得して、findViewById でBeChangeFragmentView を
ゲット、やったぜ。
Fragment とか、MainActivity のl ayout 静的に配置するとアプリが落ちて、半日以上はまったけど、できるようになってきた。
ここら辺の描画の仕方とか、タッチの処理とか システムがどう処理しているのか、View とか Fragment がどういう場所で実行され、
なにが使えるのかとか、まだまだ全然わからないよ……。Fragment に View を配置しているのは再利用をしたいと思っているから
だけど、なんか複雑にしているだけの気もする。
