(use-modules
  (srfi srfi-1)
  (srfi srfi-26)
  (ice-9 match)
  (sat solver)
  (sat helpers))

(define (get-value board vals col row)
  (1+
   (find
     (lambda (possible-value)
       (array-ref vals
                  (array-ref board col row possible-value)))
     (iota 9))))


(define (set-initial-value board col row val)
  (add-clause
    (list
      (array-ref board
                 col
                 row
                 (1- val)))))


(define (make-row row)
  (map
    (cut cons <> row)
    (iota 9)))


(define (make-col col)
  (map
    (cut cons col <>)
    (iota 9)))


(define (rows)
  (map
    (cut make-row <>)
    (iota 9)))


(define (cols)
  (map
    (cut make-col <>)
    (iota 9)))


(define (make-box bcol brow)
  (let ((l '()))
    (do ((icol 0 (1+ icol))) ((= icol 3))
      (do ((irow 0 (1+ irow))) ((= irow 3))
        (set! l (cons
                  (cons (+ (* 3 bcol) icol)
                        (+ (* 3 brow) irow))
                  l))))
    l))


(define (boxes)
  (let ((l '()))
    (do ((bcol 0 (1+ bcol))) ((= bcol 3))
      (do ((brow 0 (1+ brow))) ((= brow 3))
        (set! l (cons
                   (make-box bcol brow)
                   l))
        ))
    l))


(define (unique-values board coords-list)
  (for-each
    (lambda (n)
      (exactly-one-true
        (map
          (lambda (coord)
            (array-ref board (car coord) (cdr coord) n))
          coords-list)))
    (iota 9)))


(define (all-unique-values board coord-lists)
  (for-each
    (cut unique-values board <>)
    coord-lists))


(define (make-board)
  (let ((board (make-array #f 9 9 9)))
    (array-map! board make-sat-variable)
    board))


(define (all-one-number board col row)
  (exactly-one-true
    (map
      (lambda (value)
        (array-ref board col row value))
      (iota 9))))


(let* ((board (make-board)))

  ;; The standard Sudoku rules
  (all-unique-values board (rows))
  (all-unique-values board (cols))
  (all-unique-values board (boxes))

  ;; Each position contains exactly one number
  (do ((col 0 (1+ col))) ((= col 9))
    (do ((row 0 (1+ row))) ((= row 9))
      (all-one-number board col row)))

  ;; Initially specified values
  (set-initial-value board 0 0 4)
  (set-initial-value board 0 7 5)
  (set-initial-value board 0 8 1)

  (set-initial-value board 1 1 3)
  (set-initial-value board 1 3 2)

  (set-initial-value board 2 8 4)

  (set-initial-value board 3 2 7)
  (set-initial-value board 3 6 6)
  (set-initial-value board 3 7 2)

  (set-initial-value board 4 4 8)
  (set-initial-value board 4 5 1)

  (set-initial-value board 5 6 3)

  (set-initial-value board 6 0 8)
  (set-initial-value board 6 4 4)

  (set-initial-value board 7 3 6)
  (set-initial-value board 7 6 7)

  (set-initial-value board 8 0 5)

  (let ((vals (solve-sat)))
    (do ((row 0 (1+ row))) ((= row 9))
      (do ((col 0 (1+ col))) ((= col 9))
        (format #t "~a" (get-value board vals col row)))
      (newline))))