Initial commit

3 files changed, 121 insertions, 0 deletions

diff --git a/guile/sat/helpers.scm b/guile/sat/helpers.scm
new file mode 100644
index 0000000..6729382
--- /dev/null
+++ b/guile/sat/helpers.scm
@@ -0,0 +1,19 @@
+(define-module (sat helpers)
+  #:use-module (sat solver)
+  #:use-module (srfi srfi-1)
+  #:export (exactly-one-true))
+
+(define (exactly-one-true v)
+
+  ;; At least one of 'v' must be true
+  (add-clause v)
+
+  ;; At least one of each pair in 'v' must be false
+  (pair-for-each
+    (lambda (v1p)
+      (for-each
+        (lambda (v2)
+          (add-clause (list (- (car v1p)) (- v2))))
+        (cdr v1p)))
+    v))
+
diff --git a/guile/sat/solver.scm b/guile/sat/solver.scm
new file mode 100644
index 0000000..24eb7b1
--- /dev/null
+++ b/guile/sat/solver.scm
@@ -0,0 +1,49 @@
+(define-module (sat solver)
+  #:use-module (ice-9 popen)
+  #:use-module (ice-9 rdelim)
+  #:use-module (ice-9 format)
+  #:export (solve-sat
+             make-sat-variable
+             add-clause))
+
+
+(define last-variable (make-parameter #f))
+(define sat-clauses (make-parameter #f))
+
+
+(define (make-sat-variable)
+  (unless (last-variable)
+    (error "make-variable used outside solve-sat"))
+  (last-variable (1+ (last-variable)))
+  (last-variable))
+
+
+(define (add-clause clause)
+  (sat-clauses (cons clause (sat-clauses))))
+
+
+(define (write-dimacs n-variables clauses)
+  (with-output-to-file
+    "dimacs.cnf"
+    (lambda ()
+      (format #t "p cnf ~a ~a\n"
+              n-variables
+              (length clauses))
+      (for-each (lambda (clause)
+                  (format #t "~{~d ~}0\n" clause))
+                clauses)))
+  (let loop ((port (open-pipe* OPEN_READ "kissat" "dimacs.cnf")))
+    (let ((line (read-line port)))
+      (unless (eof-object? line)
+        (format #t "Line '~a'\n" line)
+        (loop port)))))
+
+
+(define-syntax solve-sat
+  (syntax-rules ()
+    ((_ body ...)
+     (parameterize ((last-variable 0)
+                    (sat-clauses '()))
+       body ...
+       (write-dimacs (last-variable)
+                     (sat-clauses))))))
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)))))))