;; lib/minikanren/tests/queens-fd.sx — N-queens via CLP(FD).
;;
;; Native FD propagation makes N-queens tractable: 4-queens finds both
;; solutions instantly; 5-queens finds all 10 in seconds. Compare with
;; the naive enumerate-then-filter version in queens.sx, which struggles
;; past N=4.

(define
  fd-no-diag
  (fn
    (ci cj k)
    (fresh
      (a b)
      (fd-plus cj k a)
      (fd-plus ci k b)
      (fd-neq ci a)
      (fd-neq cj b))))

(define
  n-queens-4-fd
  (fn
    (cs)
    (let
      ((c1 (nth cs 0))
        (c2 (nth cs 1))
        (c3 (nth cs 2))
        (c4 (nth cs 3)))
      (mk-conj
        (fd-in c1 (list 1 2 3 4))
        (fd-in c2 (list 1 2 3 4))
        (fd-in c3 (list 1 2 3 4))
        (fd-in c4 (list 1 2 3 4))
        (fd-distinct cs)
        (fd-no-diag c1 c2 1)
        (fd-no-diag c1 c3 2)
        (fd-no-diag c1 c4 3)
        (fd-no-diag c2 c3 1)
        (fd-no-diag c2 c4 2)
        (fd-no-diag c3 c4 1)
        (fd-label cs)))))

(define
  n-queens-5-fd
  (fn
    (cs)
    (let
      ((c1 (nth cs 0))
        (c2 (nth cs 1))
        (c3 (nth cs 2))
        (c4 (nth cs 3))
        (c5 (nth cs 4)))
      (mk-conj
        (fd-in
          c1
          (list 1 2 3 4 5))
        (fd-in
          c2
          (list 1 2 3 4 5))
        (fd-in
          c3
          (list 1 2 3 4 5))
        (fd-in
          c4
          (list 1 2 3 4 5))
        (fd-in
          c5
          (list 1 2 3 4 5))
        (fd-distinct cs)
        (fd-no-diag c1 c2 1)
        (fd-no-diag c1 c3 2)
        (fd-no-diag c1 c4 3)
        (fd-no-diag c1 c5 4)
        (fd-no-diag c2 c3 1)
        (fd-no-diag c2 c4 2)
        (fd-no-diag c2 c5 3)
        (fd-no-diag c3 c4 1)
        (fd-no-diag c3 c5 2)
        (fd-no-diag c4 c5 1)
        (fd-label cs)))))

(mk-test
  "n-queens-4-fd-two-solutions"
  (run*
    q
    (fresh (a b c d) (== q (list a b c d)) (n-queens-4-fd (list a b c d))))
  (list
    (list 2 4 1 3)
    (list 3 1 4 2)))

(mk-test
  "n-queens-5-fd-ten-solutions"
  (let
    ((sols (run* q (fresh (a b c d e) (== q (list a b c d e)) (n-queens-5-fd (list a b c d e))))))
    (= (len sols) 10))
  true)

(mk-tests-run!)