Alloy Analyzerを使って11年前に解いた数独の問題を解き直してみたという話。
TL;DR
- 昔よりPCは速くなったし、自分も気持ちソルバを上手に使えるようになった。
- 速く答えを探すには、とにかく探さなくていいものは探すな。
経緯
過去にAlloy Analyzerを使って、「世界一難しい数独」を解いた記事を書いた。
世界一難しい数独、Alloyで解いてみたよ(RocketNews24から) - dec9ue's diary
その後、disktnkさんという方の記事で、「お前のコード超遅くね？拾ったコードでもこれくらい出るけど(意訳)」というご指摘をいただく。
＃彼は事実を書いただけ。何も悪くない。
〜11年の月日が流れる〜
急に思い出してAlloy本をさっと眺め直し、書き直してみた。← 今ここ
というわけで、久しぶりに何か書こうってわけで、改善の経緯を書いてみた。誰が読むのかは、知らない。
オリジナルコード
こんな感じで書いていた。
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って今も誰か使ってるの？
