-
Notifications
You must be signed in to change notification settings - Fork 0
/
sudoku.lisp
150 lines (129 loc) · 3.92 KB
/
sudoku.lisp
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
;;;; +----------------------------------------------------------------+
;;;; | CMSAT |
;;;; +----------------------------------------------------------------+
(in-package #:cmsat)
;; This is the Sudoku solving example from
;; https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/
;;
;; The puzzle is from
;; http://elmo.sbs.arizona.edu/sandiway/sudoku/examples.html
(defvar *sudoku-rows* 9
"The number of rows in the Sudoku board.")
(defvar *sudoku-cols* 9
"The number of columns in the Sudoku board.")
(defvar *sudoku-vals* 9
"The number of possible values in a Sudoku cell.")
(defun to-var (row col val)
"Return a variable designation for the supplied coordinates and
value."
(+ (* row *sudoku-cols* *sudoku-vals*)
(* col *sudoku-vals*)
val
1))
(defvar *clauses* '()
"List of conjuncts.")
(defvar *clause* '()
"List of disjuncts.")
(defun lit (x)
"Add a literal to the current clause."
(push x *clause*))
(defun clause ()
"Add the current clause to the list of clauses."
(when *clause*
(push *clause* *clauses*)
(setf *clause* '())))
(defun exactly-one-true ()
"Add clauses ensuring exactly one of the literals in the current
clause is true."
(let ((literals *clause*))
(clause)
(do ((i literals (cdr i)))
((null i))
(do ((j (cdr i) (cdr j)))
((null j))
(lit (- (car i)))
(lit (- (car j)))
(clause)))))
(defun rule-1 ()
"No row contains duplicate numbers."
(dotimes (row *sudoku-rows*)
(dotimes (val *sudoku-vals*)
(dotimes (col *sudoku-cols*)
(lit (to-var row col val)))
(exactly-one-true))))
(defun rule-2 ()
"No column contains duplicate numbers."
(dotimes (col *sudoku-cols*)
(dotimes (val *sudoku-vals*)
(dotimes (row *sudoku-rows*)
(lit (to-var row col val)))
(exactly-one-true))))
(defun rule-3 ()
"None of the 3x3 boxes contain duplicate numbers."
(do ((r 0 (+ r 3)))
((= r *sudoku-rows*))
(do ((c 0 (+ c 3)))
((= c *sudoku-cols*))
(dotimes (val *sudoku-vals*)
(dotimes (rr 3)
(dotimes (cc 3)
(lit (to-var (+ r rr) (+ c cc) val))))
(exactly-one-true)))))
(defun rule-4 ()
"Each position contains exactly one number."
(dotimes (row *sudoku-rows*)
(dotimes (col *sudoku-cols*)
(dotimes (val *sudoku-vals*)
(lit (to-var row col val)))
(exactly-one-true))))
(defun apply-board (initial-board)
"Add clauses for initial Sudoku board configuration."
(let ((row 0)
(col 0))
(dolist (val initial-board)
(unless (eq val '_)
(lit (to-var row col (1- val)))
(clause))
(incf col)
(when (= col *sudoku-cols*)
(setf col 0)
(incf row)))))
(defun sudoku-clauses (initial-board)
"Return the list of SAT clauses representing the Sudoku problem for
the initial board supplied."
(let ((*clauses* '())
(*clause* '()))
(rule-1)
(rule-2)
(rule-3)
(rule-4)
(apply-board initial-board)
*clauses*))
(defun print-board (assignments)
"Print a Sudoku board for the supplied variable assignment vector."
(dotimes (row *sudoku-rows*)
(dotimes (col *sudoku-cols*)
(dotimes (val *sudoku-vals*)
(let ((assignment (aref assignments (to-var row col val))))
(when assignment
(format t " ~D" (1+ val))
(return)))))
(terpri)))
(defun sudoku (initial-board)
"Print a solved Sudoku board for the supplied initial board
configuration."
(print-board (solve (sudoku-clauses initial-board))))
(defvar *example-board*
'(_ 2 _ _ _ _ _ _ _
_ _ _ 6 _ _ _ _ 3
_ 7 4 _ 8 _ _ _ _
_ _ _ _ _ 3 _ _ 2
_ 8 _ _ 4 _ _ 1 _
6 _ _ 5 _ _ _ _ _
_ _ _ _ 1 _ 7 8 _
5 _ _ _ _ 9 _ _ _
_ _ _ _ _ _ _ 4 _)
"A particularly fun puzzle.")
(defun example ()
"Demonstrate Sudoku-as-SAT-problem."
(sudoku *example-board*))