世界一難しい数独、Alloyで解いてみたよ(RocketNews24から)
RocketNews24さんで 本当に解ける人いるの？ フィンランド人数学者が作った “世界一難しい数独” が発表されるという記事があったんで以前のAlloyの記事で使ったモデルを流用して解いてみた。
about alloy Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.
- 結論：
- 実は自分は数独のルールをわかっていなかった。
- 前回より工夫したところ：
- 数字をOne,Twoといったような表記ではなく、C01とか数字が入った表現にした。
- 数独って、9x9の枠の中でカブっちゃいけない、ってルールがあったんだ。。。。ということに気づいてルールを追加した。orz
では、以前のモデルを一部流用して解いてみます。
↓9x9のグルーピングを追加
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{}
縦、横の重複禁止ルールの他に9x9の重複禁止ルールを追加
// 縦横の禁止
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]))
}
// 9x9の重複禁止
fact{
all c1,c2:G01, r1,r2:G01 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
fact{
all c1,c2:G01, r1,r2:G02 | (r1=r2 and c1=c2)or(not(cell[c1,r1]=cell[c2,r2]))
}
:
実際に解かせてみると。。。。
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秒。
チェック結果掲載できてませんが、解答ページを見てみるとちゃんとあっていました。
ちなみに、標準的な問題を解かせてみると。。。
Executing "Run run$1 for 13" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 77309 vars. 2201 primary vars. 146933 clauses. 3712ms. . found. Predicate is consistent. 49608ms.
50秒。
つまり、世界一難しい問題は、SATソルバからみると60～70%程度難しい問題だってことがわかりました。
いずれにせよ、Alloyって戦略を明示しなくてもいいのにコレぐらいの時間で数独が解けてしまいます。数独はAlloyがとても良くハマる問題だといえるのではないかと思います。
追記： 2012/07/04 回答の図をアップしました。あと、Alloyの説明をちょっと追加。
