1 files changed, 53 insertions, 0 deletions
diff --git a/sudoku.scm b/sudoku.scm
new file mode 100644
index 0000000..d759fa7
--- /dev/null
+++ b/sudoku.scm
@@ -0,0 +1,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)))))))