(use-modules
  (srfi srfi-1)
  (srfi srfi-26)
  (ice-9 match)
  (ice-9 textual-ports)
  (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 (exactly-one-number board col row)
  (exactly-one-true
    (map
      (lambda (value)
        (array-ref board col row value))
      (iota 9))))


(define (char->number c)
  (match c
         (#\0 0)
         (#\1 1)
         (#\2 2)
         (#\3 3)
         (#\4 4)
         (#\5 5)
         (#\6 6)
         (#\7 7)
         (#\8 8)
         (#\9 9)))

(define (process-line board row line)
  (map
    (lambda (c col)
      (when (char-numeric? c)
        (set-initial-value
          board
          col
          row
          (char->number c))))
    (string->list line)
    '(0 1 2 _ 3 4 5 _ 6 7 8)))


(define (read-sudoku port board)
  (process-line board 0 (get-line port))
  (process-line board 1 (get-line port))
  (process-line board 2 (get-line port))
  (get-line port)
  (process-line board 3 (get-line port))
  (process-line board 4 (get-line port))
  (process-line board 5 (get-line port))
  (get-line port)
  (process-line board 6 (get-line port))
  (process-line board 7 (get-line port))
  (process-line board 8 (get-line port)))


(define (print-sudoku board vals)
  (do ((row 0 (1+ row))) ((= row 9))
    (do ((col 0 (1+ col))) ((= col 9))
      (format #t "~a" (get-value board vals col row))
      (when (or (= col 2)
                (= col 5))
        (display "|")))
    (newline)
    (when (or (= row 2)
              (= row 5))
      (display "-----------\n"))))


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

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

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

  ;; Initially specified values
  (read-sudoku
    (open-input-file "input.sudoku")
    board)

  (let ((vals (solve-sat)))
    (print-sudoku board vals)))