Alloyでパズル (2) 数独 でテーブルビューで結果が見やすく表示できるようになったのはよかった。
が、やはり結果だけでなく問題も見たい！
問題表示の方が難しい
「明示されていない値は不定」な Alloy で、ヒントとして与えられていないセルを空にして見せる方法が思いつかなかった。
しかしようやく意味がわかるようになった イラストロジックをAlloyで解く を読んでいて、なるほどと思った。
リスト
テーブルビューで見やすく表示することを最優先しているため、本体と同様に少々力技な書き方になっている（行,列とも０〜８でなく、１〜９にしたかった）。
しかしその分読みづらさは軽減されているのではないだろうか。
// 数独 with Hint表
abstract sig Hint {C1,C2,C3,C4,C5,C6,C7,C8,C9:lone Int}
one sig R1,R2,R3,R4,R5,R6,R7,R8,R9 extends Hint {}
pred setHint[hint: set Int->Int->Int] { // row->col->value
let row = (1->R1 + 2->R2 + 3->R3 + 4->R4 + 5->R5 + 6->R6 + 7->R7 + 8->R8 + 9->R9),
col = (1->C1 + 2->C2 + 3->C3 + 4->C4 + 5->C5 + 6->C6 + 7->C7 + 8->C8 + 9->C9) |
all r,c:row.univ {
(row[r]).(col[c]) = hint[r,c] // Hint表へセット
some hint[r,c] => setCell[r,c,hint[r,c]] // Result表へセット
}
}
// 行内各列(r1.c1, r1.c2, r1.c3, ...)の値はすべて異なる (左のdisj)
// 各行同列(r1.c1, r2.c1, r3.c1, ...)の値もすべて異なる (右のdisj)
abstract sig Result {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 Result {}
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
}
pred setCell[r,c,value: Int] {
let row = (1->r1 + 2->r2 + 3->r3 + 4->r4 + 5->r5 + 6->r6 + 7->r7 + 8->r8 + 9->r9),
col = (1->c1 + 2->c2 + 3->c3 + 4->c4 + 5->c5 + 6->c6 + 7->c7 + 8->c8 + 9->c9) |
(row[r]).(col[c]) = value
}
let cell[row,col,value] = row->col->value
example1: run { // 世界一難しい
setHint[
cell[1,1,4] + cell[1,4,1] + cell[1,9,8] +
cell[2,2,7] + cell[2,3,8] + cell[2,5,6] + cell[2,7,4] + cell[2,8,2] +
cell[3,9,3] +
cell[4,6,7] +
cell[5,2,3] + cell[5,5,2] + cell[5,6,1] +
cell[6,5,5] +
cell[7,1,2] + cell[7,2,5] + cell[7,4,4] + cell[7,8,3] + cell[7,9,1] +
cell[8,3,6] + cell[8,5,3] + cell[8,8,8] +
cell[9,6,6] + cell[9,7,5] + cell[9,8,7]
]
} for 5 int
example2: run { // 藤原博文氏作
setHint[
cell[2,2,4] + cell[2,3,3] + cell[2,7,6] + cell[2,8,7] +
cell[3,1,5] + cell[3,4,4] + cell[3,6,2] + cell[3,9,8] +
cell[4,1,8] + cell[4,5,6] + cell[4,9,1] +
cell[5,1,2] + cell[5,9,5] +
cell[6,2,5] + cell[6,8,4] +
cell[7,3,6] + cell[7,7,7] +
cell[8,4,5] + cell[8,6,1] +
cell[9,5,8]
]
} for 5 int
結果
余計なものを一切見せない方針も、パズル的。
