blob: d759fa74fbb1a3f4532ab12a8423c1ab96bad8fe (
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
|
(use-modules
(sat solver)
(sat helpers))
;; Board indices: column row value
(define board-size 9)
(solve-sat
(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 loop ((l '()))
(do ((col1 0 (+ 3 col1))) ((= col1 3))
(do ((row1 0 (+ 3 row1))) ((= row1 3))
(loop (cons (array-ref board
(+ col col1)
(+ row row1))
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)))))))
|
