(use-modules
  (srfi srfi-1)
  (sat solver)
  (sat helpers))

;; Board indices: column row value
(define board-size 9)


(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))
    (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 ((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)
                                         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)))))

  (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))))