blob: 965e8d236c7bc29c3f0dd42374d694b10ffd286e (
plain)
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
(use-modules
(srfi srfi-1)
(sat solver)
(sat helpers))
;; Board indices: column row value
(define board-size 9)
(define (get-value board vals col row)
(1+
(find
(lambda (possible-value)
(array-ref vals
(array-ref board col row possible-value)))
(iota board-size))))
(define (set-initial-value board col row val)
(add-clause
(list
(array-ref board
col
row
(1- val)))))
(let ((board (make-array #f
board-size
board-size
board-size)))
(array-map! board make-sat-variable)
;; No row contains duplicate values
(do ((row 0 (1+ row))) ((= row board-size))
(do ((value 0 (1+ value))) ((= value board-size))
(exactly-one-true
(map
(lambda (col)
(array-ref board col row value))
(iota board-size)))))
;; No column contains duplicate values
(do ((col 0 (1+ col))) ((= col board-size))
(do ((value 0 (1+ value))) ((= value board-size))
(exactly-one-true
(map
(lambda (row)
(array-ref board col row value))
(iota board-size)))))
;; No 3x3 box contains duplicate values
(do ((col 0 (+ 3 col))) ((= col board-size))
(do ((row 0 (+ 3 row))) ((= row board-size))
(do ((value 0 (1+ value))) ((= value board-size))
(exactly-one-true
(let ((l '()))
(do ((col1 0 (1+ col1))) ((= col1 3))
(do ((row1 0 (1+ row1))) ((= row1 3))
(set! l (cons (array-ref board
(+ col col1)
(+ row row1)
value)
l))))
l)))))
;; Each position contains exactly one number
(do ((col 0 (1+ col))) ((= col board-size))
(do ((row 0 (1+ row))) ((= row board-size))
(exactly-one-true
(map
(lambda (value)
(array-ref board col row value))
(iota board-size)))))
;; Initially specified values
(set-initial-value board 0 0 4)
(set-initial-value board 0 7 5)
(set-initial-value board 0 8 1)
(set-initial-value board 1 1 3)
(set-initial-value board 1 3 2)
(set-initial-value board 2 8 4)
(set-initial-value board 3 2 7)
(set-initial-value board 3 6 6)
(set-initial-value board 3 7 2)
(set-initial-value board 4 4 8)
(set-initial-value board 4 5 1)
(set-initial-value board 5 6 3)
(set-initial-value board 6 0 8)
(set-initial-value board 6 4 4)
(set-initial-value board 7 3 6)
(set-initial-value board 7 6 7)
(set-initial-value board 8 0 5)
(let ((vals (solve-sat)))
(do ((row 0 (1+ row))) ((= row board-size))
(do ((col 0 (1+ col))) ((= col board-size))
(format #t "~a" (get-value board vals col row)))
(newline))))
|
