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>タグで間延びしてたのが気になったのでちょっと修正してみた。


抽象によるソフトウェア設計−Alloyではじめる形式手法−