#lang bcdc

(define n 8)
(define q (ι 'q))

; there is exact one queen in every row
(define rows
  (for/list
    ([y (in-range n)])
    (∃!
      (for/list ([x (in-range n)]) (q y x)))))

; there is exact one queen in every column
(define columns
  (for/list ([x (in-range n)])
            ; NOTE: we can omit the at most one condition, but this
            ; doesn't necessarily incur optimization on the sat solver side.
            ;
            ; (∃≥1
            (∃!
              (for/list ([y (in-range n)])
                        (q y x)))))

; there is at most one queen on every diagonal
(define diagonals
  (for*/list ([r1 (in-range n)]
              [c1 (in-range n)]
              [r2 (in-range (add1 r1) n)]
              [c2 (in-range n)]
              #:when (= (abs (- r1 r2))
                        (abs (- c1 c2))))
             (∃≤1 (list (q r1 c1) (q r2 c2)))))

(define model (all (append rows columns diagonals)))

(write-dimacs "nqueens-8.cnf" model)