Alloyでナンプレ
nishioさんのAlloyネタを追っかけてナンプレ(数独)をAlloyで写経してみた。
sig Col extends Index
とか
one sig One,Two,Three,Four,Five,Six,Seven,Eight,Nine
あたりがダサさが極まっていてたまらない。
abstract sig Index {}
sig Col extends Index {
cell : Index -> Index
}
one sig
One,Two,Three,Four,Five,Six,Seven,Eight,Nine
extends Col{}
fact{
all c : Col , row : Index | one cell[c,row]
}
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]))
}
fact {
(cell[One,One]=Four)
// 中略…
and
(cell[Two,Nine]=Four)
}
run{} for 13実行結果。
Executing "Run run$1 for 13" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 72602 vars. 2201 primary vars. 137690 clauses. 1966ms. Instance found. Predicate is consistent. 57174ms.
コードhttps://github.com/dec9ue/alloy-example/blob/master/num_ple2.als
Pythonでは10msecくらいで解けるようなので単純比較はできないけど少なくとも5000倍の開きがあります。しかし、ルール定義がたかだか20行ぐらいで済んでしまうあたり、生産性の大きな差を感じます。
Solving Every Sudoku Puzzle
2013-04-22 <pre>タグで間延びしてたのが気になったのでちょっと修正してみた。