ネットで見かけた数独の例は、妙に難しい書き方になっていた。
しかし自分で書いてみたら、シンプルなルールはシンプルに書けた。
たぶん、当時は Table View がなくて見やすい形にできなかったのだろう。
ルール説明とかいらないだろうと思うので、いきなりリストを。
puzzle2.als
/* 数独 */
// 行内各列(r1.c1, r1.c2, r1.c3, ...)の値はすべて異なる (左のdisj)
// 各行同列(r1.c1, r2.c1, r3.c1, ...)の値もすべて異なる (右のdisj)
abstract sig Row {disj c1,c2,c3,c4,c5,c6,c7,c8,c9: disj (1+2+3+4+5+6+7+8+9)}
one sig r1,r2,r3,r4,r5,r6,r7,r8,r9 extends Row {}
fact {
// 各 3x3 領域の数字はそれぞれ９種類
#(r1+r2+r3).(c1+c2+c3) = 9
#(r1+r2+r3).(c4+c5+c6) = 9
#(r1+r2+r3).(c7+c8+c9) = 9
#(r4+r5+r6).(c1+c2+c3) = 9
#(r4+r5+r6).(c4+c5+c6) = 9
#(r4+r5+r6).(c7+c8+c9) = 9
#(r7+r8+r9).(c1+c2+c3) = 9
#(r7+r8+r9).(c4+c5+c6) = 9
#(r7+r8+r9).(c7+c8+c9) = 9
}
例: run {
r1.c1=4 && r1.c4=1 && r1.c9=8
r2.c2=7 && r2.c3=8 && r2.c5=6 && r2.c7=4 && r2.c8=2
r3.c9=3
r4.c6=7
r5.c2=3 && r5.c5=2 && r5.c6=1
r6.c5=5
r7.c1=2 && r7.c2=5 && r7.c4=4 && r7.c8=3 && r7.c9=1
r8.c3=6 && r8.c5=3 && r8.c8=8
r9.c6=6 && r9.c7=5 && r9.c8=7
} for 5 int
ノーヒント: run {} for 5 int
結果の見やすさを求めて整数1〜9を使うようにしたので、9を表せる5ビット整数（for 5 int）を指定した。
例 を実行して Table View で見ると以下のように表示される。
解くのに１秒もかからないので「r1.c1=1 && r2.c2=2 && ... && r9.c9=9に解はあるのか」など、気になったらすぐに試せる。
例えば.. 本当に解ける人いるの？ フィンランド人数学者が作った“世界一難しい数独”が発表される
世界一難しい: run {
r1.c1=8
r2.c3=3 && r2.c4=6
r3.c2=7 && r3.c5=9 && r3.c7=2
r4.c2=5 && r4.c6=7
r5.c5=4 && r5.c6=5 && r5.c7=7
r6.c4=1 && r6.c8=3
r7.c3=1 && r7.c8=6 && r7.c9=8
r8.c3=8 && r8.c4=5 && r8.c8=1
r9.c2=9 && r9.c7=4
} for 5 int
瞬殺。
「数独が難しいとか意味わかんない」（Alloyさん談）