-
Notifications
You must be signed in to change notification settings - Fork 0
/
sudoku.smtl
61 lines (50 loc) · 1.01 KB
/
sudoku.smtl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
// 数独をとく SMT ソルバ
package smtl
func main() {
// c00 c01 c02
// c10 c11 c12
// c20 c21 c22
var c00, c01, c02 int
var c10, c11, c12 int
var c20, c21, c22 int
// 値の範囲
assert(c00>=1 && c00<=9)
assert(c01>=1 && c01<=9)
assert(c02>=1 && c02<=9)
assert(c10>=1 && c10<=9)
assert(c11>=1 && c11<=9)
assert(c12>=1 && c12<=9)
assert(c20>=1 && c20<=9)
assert(c21>=1 && c21<=9)
assert(c22>=1 && c22<=9)
// c00 〜 c22 は一意な値
assert(distinct(c00, c01, c02, c10, c11, c12, c20, c21, c22))
// 判明している値
assert(c00 == 4)
assert(c12 == 7)
// 横の合計=15
assert(c00+c01+c02 == 15)
assert(c10+c11+c12 == 15)
assert(c20+c21+c22 == 15)
// 縦の合計=15
assert(c00+c10+c20 == 15)
assert(c01+c11+c21 == 15)
assert(c02+c12+c22 == 15)
// 斜めの合計=15
assert(c00+c11+c22 == 15)
assert(c02+c11+c20 == 15)
}
/*
c00 = 4
c01 = 9
c02 = 2
c10 = 3
c11 = 5
c12 = 7
c20 = 8
c21 = 1
c22 = 6
4,9,2
3,5,7
8,1,6
*/