Alloy Analyzerを使って11年前に解いた数独の問題を解き直してみたという話。
TL;DR
- 昔よりPCは速くなったし、自分も気持ちソルバを上手に使えるようになった。
- 速く答えを探すには、とにかく探さなくていいものは探すな。
オリジナルコード
こんな感じで書いていた。
abstract sig Index {}
sig Col extends Index {
cell : Index -> Index
}
abstract sig G01,G02,G03 extends Col {}
one sig C01,C02,C03 extends G01{}
one sig C04,C05,C06 extends G02{}
one sig C07,C08,C09 extends G03{}
// 縦横の禁止
fact{
all c:Col, r1,r2:Index | (r1=r2)or(not(cell[c,r1]=cell[c,r2]))
}
fact{
all c1,c2:Col, r:Index | (c1=c2)or(not(cell[c1,r]=cell[c2,r]))
}
以降長くなるので略です。
当時の実行結果
Executing "Run run$1 for 13"
Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
77305 vars. 2201 primary vars. 146903 clauses. 3635ms.
. found. Predicate is consistent. 82243ms.
82秒。。。。これは当時でもクソ遅いNetbook(Aspire One)で実行した結果である。今はなきAtomコア。ああ、遅い。
現在の実行結果
同じ内容を手元のPCで動かしてみた。
Executing "Run run$1 for 13"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 Mode=batch
77887 vars. 2201 primary vars. 148957 clauses. 613ms.
. found. Predicate is consistent. 24154ms.
24秒ってことで、3.4倍くらい速くなりましたね。こいつはRyzen5 3400Gコアです。
これが11年間の歩みってやつですか。
コードを改造
Alloy本をさっと眺め読み、自分の思いつく範囲で速くなりそうな施策を打ってみた。
変更点:
- sig Colにabstractをつけた
- このシグニチャは基底のシグニチャであり、直接属するアトムは必要ない。余計な探索を生む可能性がある。というか、つけ忘れである。
- 縦横の重複防止を論理式ではなく、枝刈りができそうな表現に直してみた
- 制約事項を論理式で書くと出てきたものを評価してから落とすしかなくなる。そうではなく、最初から探索空間を制限するような制約にすることで高速化できる可能性が高い。
abstract sig Index {}
abstract sig Col extends Index {
cell : Index -> Index
}
:
// 縦横の禁止
fact{
all c:Col, v:Index | one c.cell.v
}
fact{
all r:Index, v:Index | one cell.v.r
}
実行結果
Executing "Run run$1 for 13"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 Mode=batch
11809 vars. 729 primary vars. 22923 clauses. 66ms.
. found. Predicate is consistent. 60ms.
60ms。400倍くらい速くなりました。ヨカッタね!
ところで、「拾いものコード」よりは速くなったのかな?
「拾いものコード」との比較
比較としてdisktnkさんの記事にあったコードをそのまま動かしてみた。
Executing "Run game"
Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch
2725 vars. 729 primary vars. 3303 clauses. 14ms.
. found. Predicate is consistent. 1748ms.
無事、改善後のコードは「拾いものコード」に対して30倍のスコアを叩き出しているようです。
しかし結局、私のコードと速度が違ったのはなぜだろうか?改めて見返してわからない部分もあった。
#彼の実行結果と現在の実行結果は1.5倍くらいの改善で、彼のPCは当時の私のPCの2倍以上速かったことが想像できますが、それは置いといて。
「とりあえずabstract」コードとの比較
わからないけど、とりあえず、この「拾いものコード」にはちゃんとabstractがつけてあることに気づいた。そこで、「オリジナルにabstractをちゃんとつけただけのコード」を動かしてみた。
変更前
sig Col extends Index {
:
↓
変更後
abstract sig Col extends Index {
:
実行結果
Executing "Run run$1 for 13"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20 Mode=batch
19261 vars. 729 primary vars. 36045 clauses. 145ms.
. found. Predicate is consistent. 832ms.
実行結果は「拾いものコード」より速くなった。
はぁ、まぁ、つまり、過去のスピードの差はabstractのつけ忘れだったってことで。
なお、これをつけるだけでオリジナルより30倍速いということですね。
まぁ一応
- abstractは忘れずにつけろってことだし、そこから枝を刈れば更に速くなるってこと。
- あと、Alloy Analyzerって今も誰か使ってるの?
まとめ
- 11年前よりPCは速くなった。それは3.4倍とも言えるし、1.5倍とも言える。
- とにかく探さなくていいものは探さない。
- 適切に枝刈りをすることで求解は加速する。
- abstractつけ忘れるな、abstractつけ忘れるな。
- 「世界一難しい数独」がSATソルバに解かれる時間は、まばたきよりも遥かに短い。
- Alloyって誰か使ってるの?生者でまだ使っている方はお教えください。
以上です。