From 15079ef823be474482ac7042780da43150cb58d4 Mon Sep 17 00:00:00 2001
From: Thomas White <taw@physics.org>
Date: Sun, 27 Mar 2022 19:29:46 +0200
Subject: Working solver

---
 guile/sat/solver.scm | 59 ++++++++++++++++++++++---------
 sudoku.scm           | 98 +++++++++++++++++++++++++++++++---------------------
 2 files changed, 100 insertions(+), 57 deletions(-)

diff --git a/guile/sat/solver.scm b/guile/sat/solver.scm
index 24eb7b1..f633c31 100644
--- a/guile/sat/solver.scm
+++ b/guile/sat/solver.scm
@@ -3,17 +3,16 @@
   #:use-module (ice-9 rdelim)
   #:use-module (ice-9 format)
   #:export (solve-sat
+             sat-context
              make-sat-variable
              add-clause))
 
 
-(define last-variable (make-parameter #f))
-(define sat-clauses (make-parameter #f))
+(define last-variable (make-parameter 0))
+(define sat-clauses (make-parameter '()))
 
 
 (define (make-sat-variable)
-  (unless (last-variable)
-    (error "make-variable used outside solve-sat"))
   (last-variable (1+ (last-variable)))
   (last-variable))
 
@@ -22,28 +21,54 @@
   (sat-clauses (cons clause (sat-clauses))))
 
 
-(define (write-dimacs n-variables clauses)
+(define (vline->integers line)
+  (cdr
+    (map string->number
+         (string-split line #\space))))
+
+
+(define (set-values! value-array values)
+  (for-each
+    (lambda (val)
+      ;; If exactly zero, don't set anything
+      (cond
+        ((> val 0)
+         (array-set! value-array #t val))
+        ((< val 0)
+         (array-set! value-array #f (- val)))))
+    values))
+
+
+(define* (solve-sat #:key (solver "kissat"))
+
+  ;; Prepare CNF input
   (with-output-to-file
     "dimacs.cnf"
     (lambda ()
       (format #t "p cnf ~a ~a\n"
-              n-variables
-              (length clauses))
+              (last-variable)
+              (length (sat-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)))))
+                (sat-clauses))))
+
+  ;; Run the solver and parse output
+  (let ((values (make-array 'none (list 0 (last-variable)))))
+    (let loop ((port (open-pipe* OPEN_READ solver "dimacs.cnf")))
+      (let ((line (read-line port)))
+        (unless (eof-object? line)
+          (cond
+            ((char=? (string-ref line 0) #\v)
+             (set-values! values (vline->integers line)))
+            ((string=? line "s UNSATISFIABLE")
+             (error "Unsatsfiable!")))
+          (loop port))))
+    values))
 
 
-(define-syntax solve-sat
+(define-syntax sat-context
   (syntax-rules ()
     ((_ body ...)
      (parameterize ((last-variable 0)
                     (sat-clauses '()))
-       body ...
-       (write-dimacs (last-variable)
-                     (sat-clauses))))))
+       body ...))))
diff --git a/sudoku.scm b/sudoku.scm
index d759fa7..7b1743c 100644
--- a/sudoku.scm
+++ b/sudoku.scm
@@ -1,53 +1,71 @@
 (use-modules
+  (srfi srfi-1)
   (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)))))
+(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))))
+
+
+(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))
+  ;; 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
-          (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
+          (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))
-                              l)))))))))
+                                         (+ 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)))))))
+  ;; 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)))))
+
+  (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))))
-- 
cgit v1.2.3