Sudokuシリーズその2, 頑張れSplr

何の調べ物をしていたのか忘れましたが、偶然こんなものを見つけました。 http://labs.timedia.co.jp/2017/07/sat25x2520.html

+--------------+--------------+--------------+--------------+--------------+
| . 12  .  .  .| .  .  .  .  .| .  .  .  9  .| .  . 15  .  .|22  .  .  .  .|
| .  .  .  .  .| .  9  . 19  .| .  . 10 11  .| .  .  .  .  .| .  .  .  .  .|
| .  4  . 22  .| .  .  .  .  .| .  .  .  .  .| .  . 12  .  .|20 15  1  .  .|
|16  1 20 15  .| .  .  .  .  .| .  .  .  .  .|14  .  4  . 22|12 25  .  .  .|
| .  .  .  .  .| .  7  2 11  .|23  . 19  8  .| .  .  . 13  .| .  .  .  .  .|
+--------------+--------------+--------------+--------------+--------------+
|13  .  8  .  2| .  .  .  .  .| .  .  7 23  6| .  9  . 19 11| .  .  .  .  .|
| .  .  .  . 23| .  .  .  . 16| .  .  .  .  .| .  .  .  .  .| 1  .  .  .  .|
| 7  .  .  . 10| 3  .  .  .  .| .  .  9 19  .| . 13  . 23  .| .  .  .  5  .|
| .  .  .  .  .|15  .  .  . 22| .  .  .  .  .| .  .  .  .  .|25 20  .  .  .|
| .  .  .  .  .|12  . 14  1 25| .  .  .  .  .| .  .  3  .  .|16  4 15  .  .|
+--------------+--------------+--------------+--------------+--------------+
| .  .  .  .  .| . 19  9  .  .| .  . 13  7  .| .  .  .  5  .| .  .  . 23 10|
| . 22  . 25 17| .  .  .  .  .| .  .  .  .  .|12  . 20  .  .| .  .  .  .  .|
| . 20 12 16  .| .  .  .  .  .| .  .  .  . 14|15 22  1  . 25| .  .  .  .  .|
| . 15  .  .  .| . 11  .  .  .| .  .  .  .  .| .  . 16  .  .| .  .  .  9  .|
| .  .  .  1  .| . 10  . 23  .| .  .  .  . 18| .  .  .  .  .| .  .  .  .  8|
+--------------+--------------+--------------+--------------+--------------+
|10  .  .  .  8| . 13  .  5  .| .  .  .  .  .| . 19  . 11 23| .  .  .  6  .|
| .  .  . 17  7| .  .  .  .  .| .  .  .  .  1| .  .  .  .  .| 4 22  .  .  .|
| .  .  .  . 11| . 23  .  .  .| .  .  .  . 20| .  .  .  2  .|14  .  .  .  .|
|19  . 23  .  5| .  8  .  9  .| . 21  .  .  .| . 10  .  7  .| .  .  .  .  .|
| .  3  .  .  .| .  .  .  .  .|25  4  .  . 12| .  .  .  .  .|15  1 16  .  .|
+--------------+--------------+--------------+--------------+--------------+
| .  .  .  .  .| .  .  .  . 15| . 12  .  . 25| 1  . 22  .  .| 3  .  .  .  .|
|23  .  .  . 19| .  2  .  .  .| .  .  .  .  .| .  .  . 10  .| .  .  .  7 11|
| .  .  . 18  .| .  .  .  .  .| . 20  .  .  .| .  .  .  .  .| .  .  .  .  .|
| .  .  .  .  .| .  .  .  .  4|14 15  .  . 22| .  .  .  .  .| .  .  . 10  .|
|11  .  .  .  9| .  .  .  .  .| .  .  .  .  .| .  .  .  .  .| .  .  . 19  .|
+--------------+--------------+--------------+--------------+--------------+

この問題をSATで解く（正確には、他の人に解いてもらう）という話です。

さて、制約充足問題というと、すぐに思いつくのがSATであろう。ということで調べると、SATでパズルを解く研究をしている神戸大学情報基盤センターが直ぐに見つかる。

「SATでパズルを解く研究をしている」という表現はどうなのかと思わないでもないけどもそれは置いといて、田村先生によって20秒で解かれてしまったそうだ。

さて、Splrだとどうだろうか。面白そうなのでやってみました。

Sudokuの符号化(part 1)

Sudokuのルールは以下の4つ。

セルには一つの数を割り当てる（単一制約）
行には全ての数をそれぞれ一回のみ割り当てる（行制約）
列には全ての数をそれぞれ一回のみ割り当てる（列制約）
ブロックには全ての数をそれぞれ一回のみ割り当てる（ブロック制約）

既に何度か符号化しているものの、以前作ったものがサイズ25に対応できてなかったことがわかったのでもう一度What's Miracle Sudoku?で導入した、第１象限限定の幾何構造体Pos、その上の状態保持構造体Cellをそのまま利用して作り直し。例えばこんな感じで簡単に書ける。

for i in 1..9 {
  for j in 1..9 {
     let p = Pos::at(i, j);
     for jj in j + 1..9; 
         let q = Pos::at(i, jj);
         for d in 1..9 {
             rules.add(p.state(d, true).requires(q.state(d, false)));
         }
     }
  }
}

そして上の問題の設定は、件のブログではverbatimで与えられていたのでコピペして&strとして取り込み、スライスをうまく作ってparseするのが現実的（解くのが数秒で問題入力が1時間ではちょっとね）。

const dim: usize = 25;

const S25: &str = "
+--------------+--------------+--------------+--------------+--------------+
| . 12  .  .  .| .  .  .  .  .| .  .  .  9  .| .  . 15  .  .|22  .  .  .  .|
...
";

fn parse() -> Vec<(Pos, usize)> {
  let block_len = (dim as f64).sqrt() as usize;
  let mut i = 0;
  for (ii, l) in S25.lines().skip(1).enumerate() {
     if ii % (block_len + 1) == 0 {
         continue;
     }
     i += 1;
     ...
  }

でやってみたところ、全然だめ。いろいろ補助的なルールを追加しても5000秒でもだめ。

2020-10-13

CaDiCaLが8000秒掛かっても解けないじゃん！！こんなん解けねーよ！

2020-11-02

先月は10040あたりでピタリと停滞していたのが10150あたりまで伸びるようになってきた。

2020-11-06

10040とか10150とか言っていたのはasserted varsの個数だけど、eliminated varsのことを考えてないので正確ではない。大体残り5080くらいということ。

2020-11-07

CaDiCaLで実行すると数時間掛かった。残りが減れば加速するかと思っていたけど、CaDiCaLですら残り4000台は淡々としか減っていかない。残り3000の前半くらいからやっと終わりが見えてくる。うーむ、4000台への突入ではなく3000台を通り過ごさなければならないのか。これは長い。

2020-11-18

新しい実装で5000秒で残り5081とか10000秒で4991くらい。これはブレークスルーであるが、一方でコアがなかなか小さくならない（1100程度）ので時間を掛けても解けるかどうか自信がない。

$ splr -t 10000 sudoku25.cnf
sudoku25.cnf                                   15625,970146 |time: 10000.10
 #conflict:  108320000, #decision:    151987030, #propagate:     7602488160 
  Assignment|#rem:     4991, #ass:    10205, #elm:      429, prg%:  68.0576 
      Clause|Remv:    27129, LBD2:      291, Binc:  1020680, Perm:  1057443 
     Restart|#BLK:    44811, #RST:   383671, span:     8192, shft:    16382 
         EMA|tLBD:   1.6215, tASG:   0.9990, core:     1196, /dpc:     1.40 
    Conflict|eLBD:    32.07, cnfl:    44.64, bjmp:    43.51, /ppc:    70.19 
        misc|elim:       42, cviv:       16, #vbv:        0, /cpr:   282.31 
    Strategy|mode: HighSuccessiveConflict (long decision chains)
      Result|file: ./.ans_sudoku25.cnf
s UNKNOWN (TimeOut): sudoku25.cnf

2020-11-21

三連休は数独三昧になりそうだ。

202011-21T11:23 (Online TeXを見ながら) 5000秒で4800台とか。
202011-22T22:00 2000秒台で4800台突入。

2020-11-24

あー、あるルールを追加してなかったなあと思って生成プログラムを変更したらCaDiCaLが一瞬で解くようになった。もしかしてと思ってやってみたら、

$ splr sudoku25.cnf
sudoku25.cnf                                   15625,972021 |time:    15.03
 #conflict:        324, #decision:         2920, #propagate:         101930 
  Assignment|#rem:     2507, #ass:    13118, #elm:        0, prg%:  83.9552 
      Clause|Remv:      229, LBD2:       35, Binc:   922556, Perm:   924329 
     Restart|#BLK:        8, #RST:        0, span:        1, shft:        0 
         EMA|tLBD:  38.8489, tASG:  52.9797, core:        0, /dpc:     9.01 
    Conflict|eLBD:     4.22, cnfl:     1.17, bjmp:     0.76, /ppc:   314.60 
        misc|elim:        2, cviv:        0, #vbv:        0, /cpr:     8.31 
    Strategy|mode: Initial search phase before a main strategy
      Result|file: ./.ans_sudoku25.cnf
s SATISFIABLE: sudoku25.cnf
$ dmcr sudoku25.cnf 
A valid assignment set for sudoku25.cnf is found in .ans_sudoku25.cnf

ぎょえーーーーー、なんだったんだこの一ヶ月の電気代！！！！！！

とりあえず証拠の品を部分公開。

+--------------+--------------+--------------+--------------+--------------+
| 8 12 11 10 18|14 25  4 16 24|20 17  1  9 21|19  5 15  6  2|22 23  7  3 13|
| 2  .  .  .  .| .  9  . 19  .| .  . 10 11  .| .  .  .  .  .| .  .  .  . 21|
| 9  4  . 22  .| .  .  .  .  .| .  .  .  .  .| .  . 12  .  .|20 15  1  .  2|
|16  1 20 15  .| .  .  .  .  .| .  .  .  .  .|14  .  4  . 22|12 25  .  . 19|
|14  .  .  .  .| .  7  2 11  .|23  . 19  8  .| .  .  . 13  .| .  .  .  .  4|
+--------------+--------------+--------------+--------------+--------------+
|13  .  8  .  2| .  .  .  .  .| .  .  7 23  6| .  9  . 19 11| .  .  .  . 12|
|22  .  .  . 23| .  .  .  . 16| .  .  .  .  .| .  .  .  .  .| 1  .  .  .  7|
| 7  .  .  . 10| 3  .  .  .  .| .  .  9 19  .| . 13  . 23  .| .  .  .  5 18|
|17  .  .  .  .|15  .  .  . 22| .  .  .  .  .| .  .  .  .  .|25 20  .  .  9|
| 6  .  .  .  .|12  . 14  1 25| .  .  .  .  .| .  .  3  .  .|16  4 15  . 23|
+--------------+--------------+--------------+--------------+--------------+
| 3  .  .  .  .| . 19  9  .  .| .  . 13  7  .| .  .  .  5  .| .  .  . 23 10|
| 5 22  . 25 17| .  .  .  .  .| .  .  .  .  .|12  . 20  .  .| .  .  .  . 16|
|18 20 12 16  .| .  .  .  .  .| .  .  .  . 14|15 22  1  . 25| .  .  .  .  3|
|24 15  .  .  .| . 11  .  .  .| .  .  .  .  .| .  . 16  .  .| .  .  .  9  1|
|21  .  .  1  .| . 10  . 23  .| .  .  .  . 18| .  .  .  .  .| .  .  .  .  8|
+--------------+--------------+--------------+--------------+--------------+
|10  .  .  .  8| . 13  .  5  .| .  .  .  .  .| . 19  . 11 23| .  .  .  6 20|
|12  .  . 17  7| .  .  .  .  .| .  .  .  .  1| .  .  .  .  .| 4 22  .  .  5|
|15  .  .  . 11| . 23  .  .  .| .  .  .  . 20| .  .  .  2  .|14  .  .  . 24|
|19  . 23  .  5| .  8  .  9  .| . 21  .  .  .| . 10  .  7  .| .  .  .  . 25|
|20  3  .  .  .| .  .  .  .  .|25  4  .  . 12| .  .  .  .  .|15  1 16  . 17|
+--------------+--------------+--------------+--------------+--------------+
| 4  .  .  .  .| .  .  .  . 15| . 12  .  . 25| 1  . 22  .  .| 3  .  .  . 14|
|23  .  .  . 19| .  2  .  .  .| .  .  .  .  .| .  .  . 10  .| .  .  .  7 11|
|25  .  . 18  .| .  .  .  .  .| . 20  .  .  .| .  .  .  .  .| .  .  .  . 22|
| 1  .  .  .  .| .  .  .  .  4|14 15  .  . 22| .  .  .  .  .| .  .  . 10  6|
|11  6 14  3  9| 5 22 17 20  8|13  7 16  1 10| 2  4 23 12 18|24 21 25 19 15|
+--------------+--------------+--------------+--------------+--------------+

Sudokuの符号化(part 2)

Sudokuのルールは以下の4つ（これは再掲）：

セルには{多くとも,少なくとも}一つの数を割り当てる（最多・最少単一制約）
行には全ての数をそれぞれ一回のみ割り当てる（行制約）
列には全ての数をそれぞれ一回のみ割り当てる（列制約）
ブロックには全ての数をそれぞれ一回のみ割り当てる（ブロック制約）

ここで、2から4は以下のように解釈すべきである：

行、列、ブロックなどのグループはあるセルに一つの数が割り当てられたら、他のセルにはその数は割り当てられない（拡大最多単一制約）
行、列、ブロックなどのグループは全ての数をそれぞれ少なくとも1回割り当てる（拡大最少単一制約）

この2番目が最初のプログラムにはなかった（negative assertionsからpositive assertionへの導出がなかったので、そりゃ探索空間が小さくならないわ）。行制約の単純な解釈だと抜け落ちてしまう。それでもN=9, 16くらいだと問題にならないので、ブログなどでは出てこなくても当然かもしれない。

これが色々なソルバーの説明で出てくるXOR gateの話に繋がるのだろうか。

2020-11-25

上の説明とコードを見比べていて、無駄なルールを生成していたことに気づいたので、削除するとさらに速くなりました。

$ splr sudoku25.cnf
sudoku25.cnf                                   15625,925146 |time:     0.50
 #conflict:        314, #decision:         3452, #propagate:         110839 
  Assignment|#rem:     3967, #ass:    11658, #elm:        0, prg%:  74.6112 
      Clause|Remv:      243, LBD2:       27, Binc:   922541, Perm:   924411 
     Restart|#BLK:        7, #RST:        0, span:        1, shft:        0 
         EMA|tLBD:  41.1487, tASG:  52.2173, core:        0, /dpc:    10.99 
    Conflict|eLBD:     5.74, cnfl:     1.63, bjmp:     1.14, /ppc:   352.99 
        misc|elim:        2, cviv:        0, #vbv:        0, /cpr:    10.47 
    Strategy|mode: Initial search phase before a main strategy
      Result|file: ./.ans_sudoku25.cnf
s SATISFIABLE: sudoku25.cnf

Sudokuの符号化(part 3)

Sudokuのルールは以下の2つである：

セルには{多くとも,少なくとも}一つの数を割り当てる（最多・最少単一制約）
行、列、ブロックなどのグループには全ての数をそれぞれ{多くとも,少なくとも}一回のみ割り当てる（拡大最多・最少単一制約）

2のルールから実行時に以下が自動的に導出される：

グループにおいて、あるセルに一つの数が割り当てられたら、他のセルにはその数は割り当てられない(positive to negative implication)
グループにおいて、N-1セルにある数が割り当てられる可能性がなくなったら、残りセルにその数が割り当てられる(negatives to positive implication)

これにより探索空間が単調に減少する。

Published at 2020-08-19 Last updated 2020-11-25