Alloyでパズル (15) 数独 ふたたび

3756 ワード
数独 AlloyAnalyzer どう書く どう書く テキストリンク

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

結果

余計なものを一切見せない方針も、パズル的。
　　

参考