Sudoku solver clojure

solver.clj

(ns sat.core
  (:require [rolling-stones.core :as sat :refer [!]]
            [clojure.string :as str]))

(def rows 9)
(def cols 9)
(def values 9)


(defn possible-square-values
  "All the possible values in a square"
  [r c]
  (for [x (map inc (range values))]
    {:r r :c c :x x}))


(defn one-number-per-square []
  (for [r (range rows)
        c (range cols)]
    (sat/exactly 1 (possible-square-values r c))))


(defn each-number-once-per-row []
  (apply
   concat
   (for [row (range rows)]
     (for [x (map inc (range values))]
       (sat/exactly
        1
        (for [c (range cols)]
          {:r row :c c :x x}))))))


(defn each-number-once-per-column []
  (apply
   concat
   (for [col (range cols)]
     (for [x (map inc (range values))]
       (sat/exactly
        1
        (for [r (range rows)]
          {:r r :c col :x x}))))))


(defn box-coords [d-row d-col]
  (apply
   concat
   (for [r (range 3)]
     (for [c (range 3)]
       {:r (+ r d-row) :c (+ c d-col)}))))


(defn each-number-once-per-box []
  (apply
   concat
   (for [x (map inc (range values))]
     (for [d-row (range 0 8 3)
           d-col (range 0 8 3)]
       (sat/exactly
        1
        (for [{:keys [r c]} (box-coords d-row d-col)]
          {:r r :c c :x x}))))))


(defn render [board]
  (let [lookup (zipmap (map (juxt :r :c) board) board)
        board  (for [r (range rows)
                     c (range cols)]
                 {:r r :c c :x (:x (get lookup [r c]))})
        rows   (for [row (partition-by :r board)]
                 (->> (map #(or (:x %) ".") row)
                      (partition 3)
                      (map (partial str/join " "))
                      (str/join " | ")))
        rows   (map (partial str " ") rows)]
    (doall (map println (take 3 rows)))
    (println "-------+-------+-------")
    (doall (map println (->> rows (drop 3) (take 3))))
    (println "-------+-------+-------")
    (doall (map println (take-last 3 rows)))
    nil))


(defn solve [known]
  (filter
   sat/positive?
   (sat/solve-symbolic-cnf
    (concat (one-number-per-square)
            (each-number-once-per-row)
            (each-number-once-per-column)
            (each-number-once-per-box)
            (map vector known)))))

(comment
  (def puzzle
    [{:r 0 :c 1 :x 6}
     {:r 2 :c 0 :x 4}

     {:r 0 :c 5 :x 7}
     {:r 2 :c 5 :x 9}

     {:r 1 :c 6 :x 8}
     {:r 0 :c 7 :x 3}
     {:r 1 :c 8 :x 2}

     {:r 5 :c 0 :x 1}
     {:r 4 :c 1 :x 3}
     {:r 4 :c 2 :x 5}

     {:r 3 :c 3 :x 3}
     {:r 4 :c 3 :x 4}
     {:r 4 :c 5 :x 8}
     {:r 5 :c 5 :x 6}

     {:r 4 :c 6 :x 7}
     {:r 4 :c 7 :x 9}
     {:r 3 :c 8 :x 1}

     {:r 7 :c 0 :x 8}
     {:r 8 :c 1 :x 2}
     {:r 7 :c 2 :x 3}

     {:r 6 :c 3 :x 2}
     {:r 8 :c 3 :x 7}

     {:r 6 :c 8 :x 7}
     {:r 8 :c 7 :x 6}]))

(comment
  (render puzzle)
  (render (solve puzzle)))

Output

 . 6 . | . . 7 | . 3 .
 . . . | . . . | 8 . 2
 4 . . | . . 9 | . . .
-------+-------+-------
 . . . | 3 . . | . . 1
 . 3 5 | 4 . 8 | 7 9 .
 1 . . | . . 6 | . . .
-------+-------+-------
 . . . | 2 . . | . . 7
 8 . 3 | . . . | . . .
 . 2 . | 7 . . | . 6 .

and

 5 6 8 | 1 2 7 | 4 3 9
 3 9 7 | 6 5 4 | 8 1 2
 4 1 2 | 8 3 9 | 6 7 5
-------+-------+-------
 7 8 6 | 3 9 2 | 5 4 1
 2 3 5 | 4 1 8 | 7 9 6
 1 4 9 | 5 7 6 | 3 2 8
-------+-------+-------
 6 5 1 | 2 4 3 | 9 8 7
 8 7 3 | 9 6 1 | 2 5 4
 9 2 4 | 7 8 5 | 1 6 3