親しみやすい書き方や見やすい表示が得意で数独を瞬殺する実力も見せる Alloy さん、しかし実は数字が苦手だ。
今回はそんな苦手分野のパズル、魔方陣 を書いてみよう。
リスト
小学生の頃好きだった魔方陣は、単純なルールで記述するのは簡単。
５×５のものを書かせてみよう。
// 魔方陣 ５×５
abstract sig Row {c1,c2,c3,c4,c5: Int}
one sig r1,r2,r3,r4,r5 extends Row {}
let Col = (c1+c2+c3+c4+c5)
fact {
// １～全マス数 の全てがいずれかのマスに入る
Row.Col = prevs[mul[#Row,#Row].next] - prevs[1]
let lineSum = sum[Row.c1] {
// 各列の和は等しい
sum[Row.c2] = lineSum
sum[Row.c3] = lineSum
sum[Row.c4] = lineSum
sum[Row.c5] = lineSum
// 各行の和も等しい
all r:Row | sum[r.Col] = lineSum
// 対角線の和も等しい
sum[r1.c1 + r2.c2 + r3.c3 + r4.c4 + r5.c5] = lineSum
sum[r1.c5 + r2.c4 + r3.c3 + r4.c2 + r5.c1] = lineSum
}
}
run {} for 8 int
25 までの数字を使うので、25+24+23+22+21 を計算できる８ビット整数を指定している。
列数変化への対応しやすさや高速化などのため、何度か書き直した。
SATソルバを切り替えて比べてみると、この例ではMiniSat with Unsat Coreが一番速く、それでも２分近くかかった（遅いものでは約９分）。
６×６にすると、ちょっと試すのが嫌なくらいかかる。
もっと速い書き方をあみだしたいものだ。
結果
┌────────┬──┬──┬──┬──┬──┐
│this/Row│c1│c2│c3│c4│c5│
├────────┼──┼──┼──┼──┼──┤
│r1⁰ │20│6 │13│12│14│
├────────┼──┼──┼──┼──┼──┤
│r2⁰ │18│10│19│16│2 │
├────────┼──┼──┼──┼──┼──┤
│r3⁰ │21│9 │7 │25│3 │
├────────┼──┼──┼──┼──┼──┤
│r4⁰ │1 │23│15│4 │22│
├────────┼──┼──┼──┼──┼──┤
│r5⁰ │5 │17│11│8 │24│
└────────┴──┴──┴──┴──┴──┘
解説 : Alloyさんはなぜ数字が苦手なのか
というほどちゃんと説明できるわけではないけれど..
Alloy が通常扱える数値は -8〜7 の16通りだけである。
Alloy の大前提である小スコープ仮説（モデルの不具合のほとんどは小さい例で示すことができる）にはそれで十分であり、デフォで大きな数を扱えて重いよりも、軽量でインクリメンタルという美点に価値があると考えられているからだ。
とは言え多少は大きな数を扱えないと困る場合もあるので、実行時に整数型のビット数を指定できるようになっている（今回の8 intのように）。
Evaluator でIntやunivを見るとわかる通り、ビット数を指定しないときモデルには実際に -8〜7 までの 16 要素が含まれる。
今回のように８ビットを指定しようものなら数値だけで 256 要素含まれる。
たいていのモデルは数値以外の全要素を合わせて数個〜数十個なのに。
イメージで言うなら、Alloy さんはこれだけの数のカードをテーブルに並べて、数字が入るべきところに順次当てはめていく。
カードが増えるとものすごく手間が増えるのだ。
（効果的な並べ方や当てはまらない見切りがとてもうまいのだけれども）
そんなわけで、扱う数字が大きいことは処理時間に多大な影響をもたらす。
なるべく数を扱わず、{大きい, 適正範囲, 小さい}といった意味的・抽象的な値を扱うのが正しい Alloy との付き合い方である。