diff --git a/lib/minikanren/queens.sx b/lib/minikanren/queens.sx new file mode 100644 index 00000000..27daa3fc --- /dev/null +++ b/lib/minikanren/queens.sx @@ -0,0 +1,67 @@ +;; lib/minikanren/queens.sx — N-queens via ino + all-distincto + project. +;; +;; Encoding: q = (c1 c2 ... cn) where ci is the column of the queen in +;; row i. Each ci ∈ {1..n}; all distinct (no two queens share a column); +;; no two queens on the same diagonal (|ci - cj| ≠ |i - j| for i ≠ j). +;; +;; The diagonal check uses `project` to escape into host arithmetic +;; once both column values are ground. + +(define + safe-diag + (fn + (a b dist) + (project (a b) (if (= (abs (- a b)) dist) fail succeed)))) + +(define + safe-cell-vs-rest + (fn + (c c-row others next-row) + (cond + ((empty? others) succeed) + (:else + (mk-conj + (safe-diag c (first others) (- next-row c-row)) + (safe-cell-vs-rest c c-row (rest others) (+ next-row 1))))))) + +(define + all-cells-safe + (fn + (cols start-row) + (cond + ((empty? cols) succeed) + (:else + (mk-conj + (safe-cell-vs-rest + (first cols) + start-row + (rest cols) + (+ start-row 1)) + (all-cells-safe (rest cols) (+ start-row 1))))))) + +(define + range-1-to-n + (fn + (n) + (cond + ((= n 0) (list)) + (:else (append (range-1-to-n (- n 1)) (list n)))))) + +(define + ino-each + (fn + (cols dom) + (cond + ((empty? cols) succeed) + (:else (mk-conj (ino (first cols) dom) (ino-each (rest cols) dom)))))) + +(define + queens-cols + (fn + (cols n) + (let + ((dom (range-1-to-n n))) + (mk-conj + (ino-each cols dom) + (all-distincto cols) + (all-cells-safe cols 1))))) diff --git a/lib/minikanren/tests/queens.sx b/lib/minikanren/tests/queens.sx new file mode 100644 index 00000000..2f85bdd8 --- /dev/null +++ b/lib/minikanren/tests/queens.sx @@ -0,0 +1,45 @@ +;; lib/minikanren/tests/queens.sx — N-queens, the classic miniKanren benchmark. + +;; --- safe-diag (helper) --- + +(mk-test + "safe-diag-different-cols-different-distance" + (run* q (safe-diag 1 4 2)) + (list (make-symbol "_.0"))) + +(mk-test + "safe-diag-same-distance-fails" + (run* q (safe-diag 1 4 3)) + (list)) + +(mk-test + "safe-diag-same-distance-other-direction-fails" + (run* q (safe-diag 4 1 3)) + (list)) + +;; --- ino-each / range --- + +(mk-test + "range-1-to-4" + (range-1-to-n 4) + (list 1 2 3 4)) +(mk-test "range-empty" (range-1-to-n 0) (list)) + +;; --- 4-queens: two solutions --- + +(mk-test + "queens-4" + (let + ((sols (run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols (list a b c d) 4))))) + (and + (= (len sols) 2) + (and + (some + (fn (s) (= s (list 2 4 1 3))) + sols) + (some + (fn (s) (= s (list 3 1 4 2))) + sols)))) + true) + +(mk-tests-run!) diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md index 09af1701..35b5193d 100644 --- a/plans/minikanren-on-sx.md +++ b/plans/minikanren-on-sx.md @@ -169,6 +169,14 @@ _(none yet)_ _Newest first._ +- **2026-05-08** — **N-queens (classic miniKanren benchmark green)**: + `lib/minikanren/queens.sx`. Encoding cols(i) = column of queen in row i; + `ino-each` + `all-distincto` cover row/column constraints; `safe-diag` + uses `project` to escape into host arithmetic for the `|c_i - c_j| ≠ + |i - j|` diagonal check; `all-cells-safe` walks pairs at construction + time. `(run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols + (list a b c d) 4)))` returns the two valid 4-queens placements + `(2 4 1 3)` and `(3 1 4 2)`. 6 new tests, 243/243 cumulative. - **2026-05-08** — **Phase 6 piece A — minimal FD (ino + all-distincto)**: `lib/minikanren/fd.sx`. `ino` is `membero` with the FD-style argument order; `all-distincto` is `nafc + membero` walking the list. Together