diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx index 46fd4fff..fb2851a8 100644 --- a/lib/minikanren/clpfd.sx +++ b/lib/minikanren/clpfd.sx @@ -230,8 +230,10 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) ;; --- fd-lt --- @@ -294,8 +296,10 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) ;; --- fd-lte --- @@ -358,8 +362,10 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) ;; --- fd-eq --- @@ -428,8 +434,10 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) ;; --- labelling --- @@ -667,8 +675,10 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) ;; --- fd-times (x * y = z, ground-cases propagator) --- @@ -842,5 +852,7 @@ (let ((s2 (fd-add-constraint s c))) (let - ((s3 (c s2))) - (cond ((= s3 nil) mzero) (:else (unit s3))))))))) + ((s2-or-nil (c s2))) + (let + ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil))))) + (cond ((= s3 nil) mzero) (:else (unit s3)))))))))) diff --git a/lib/minikanren/tests/send-more-money.sx b/lib/minikanren/tests/send-more-money.sx new file mode 100644 index 00000000..9fd81cf9 --- /dev/null +++ b/lib/minikanren/tests/send-more-money.sx @@ -0,0 +1,97 @@ +;; lib/minikanren/tests/send-more-money.sx — classic cryptarithmetic +;; +;; S E N D +;; + M O R E +;; --------- +;; M O N E Y +;; +;; Column-by-column encoding with carries c1, c2, c3, and the +;; leftmost column produces a carry which equals M (the result is 5 digits). +;; All 8 letters distinct; S ≠ 0, M ≠ 0. +;; Unique solution: S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2. +;; +;; Note: the full search labelling 11 variables from {0..9} is too slow +;; for naive labelling order (10^11 combinations naively, even with +;; bounds-consistency the branching factor dominates). Real CLP(FD) +;; systems use first-fail heuristics. Here we only verify the encoding +;; against the known answer. + +(define + digits-0-9 + (list + 0 + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9)) +(define + digits-1-9 + (list + 1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9)) + +(define + smm-col-with-carry + (fn + (x y carry-in z carry-out) + (fresh + (xy xyc ten-cout z-plus-ten-cout) + (fd-plus x y xy) + (fd-plus xy carry-in xyc) + (fd-times 10 carry-out ten-cout) + (fd-plus z ten-cout z-plus-ten-cout) + (fd-eq xyc z-plus-ten-cout)))) + +(define + send-more-money + (fn + (S E N D M O R Y) + (fresh + (c1 c2 c3) + (mk-conj + (fd-in S digits-1-9) + (fd-in M digits-1-9) + (fd-in E digits-0-9) + (fd-in N digits-0-9) + (fd-in D digits-0-9) + (fd-in O digits-0-9) + (fd-in R digits-0-9) + (fd-in Y digits-0-9) + (fd-in c1 (list 0 1)) + (fd-in c2 (list 0 1)) + (fd-in c3 (list 0 1)) + (fd-distinct (list S E N D M O R Y)) + (smm-col-with-carry D E 0 Y c1) + (smm-col-with-carry N R c1 E c2) + (smm-col-with-carry E O c2 N c3) + (smm-col-with-carry S M c3 O M) + (fd-label (list S E N D M O R Y c1 c2 c3)))))) + +(mk-test + "send-more-money-verify-known-solution" + (run* + q + (send-more-money + 9 + 5 + 6 + 7 + 1 + 0 + 8 + 2)) + (list (make-symbol "_.0"))) + +(mk-tests-run!) diff --git a/lib/minikanren/tests/sudoku-4x4.sx b/lib/minikanren/tests/sudoku-4x4.sx new file mode 100644 index 00000000..771e0fc7 --- /dev/null +++ b/lib/minikanren/tests/sudoku-4x4.sx @@ -0,0 +1,89 @@ +;; lib/minikanren/tests/sudoku-4x4.sx — Sudoku 4×4 via CLP(FD). +;; +;; Grid in row-major order: +;; +;; c0 c1 | c2 c3 +;; c4 c5 | c6 c7 +;; ------+------ +;; c8 c9 | cA cB +;; cC cD | cE cF +;; +;; Each cell ∈ {1, 2, 3, 4}. 4 rows + 4 cols + 4 2x2 boxes are each a +;; distinct permutation. + +(define digits-1-4 (list 1 2 3 4)) + +(define + sudoku-4x4 + (fn + (cells) + (let + ((c0 (nth cells 0)) + (c1 (nth cells 1)) + (c2 (nth cells 2)) + (c3 (nth cells 3)) + (c4 (nth cells 4)) + (c5 (nth cells 5)) + (c6 (nth cells 6)) + (c7 (nth cells 7)) + (c8 (nth cells 8)) + (c9 (nth cells 9)) + (cA (nth cells 10)) + (cB (nth cells 11)) + (cC (nth cells 12)) + (cD (nth cells 13)) + (cE (nth cells 14)) + (cF (nth cells 15))) + (mk-conj + (fd-in c0 digits-1-4) + (fd-in c1 digits-1-4) + (fd-in c2 digits-1-4) + (fd-in c3 digits-1-4) + (fd-in c4 digits-1-4) + (fd-in c5 digits-1-4) + (fd-in c6 digits-1-4) + (fd-in c7 digits-1-4) + (fd-in c8 digits-1-4) + (fd-in c9 digits-1-4) + (fd-in cA digits-1-4) + (fd-in cB digits-1-4) + (fd-in cC digits-1-4) + (fd-in cD digits-1-4) + (fd-in cE digits-1-4) + (fd-in cF digits-1-4) + (fd-distinct (list c0 c1 c2 c3)) + (fd-distinct (list c4 c5 c6 c7)) + (fd-distinct (list c8 c9 cA cB)) + (fd-distinct (list cC cD cE cF)) + (fd-distinct (list c0 c4 c8 cC)) + (fd-distinct (list c1 c5 c9 cD)) + (fd-distinct (list c2 c6 cA cE)) + (fd-distinct (list c3 c7 cB cF)) + (fd-distinct (list c0 c1 c4 c5)) + (fd-distinct (list c2 c3 c6 c7)) + (fd-distinct (list c8 c9 cC cD)) + (fd-distinct (list cA cB cE cF)) + (fd-label cells))))) + +;; --- Tests --- + +(mk-test + "sudoku-4x4-empty-grid-count" + (let + ((sols (run* q (fresh (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF) (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)) (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)))))) + (len sols)) + 288) + +(mk-test + "sudoku-4x4-impossible-clue-empty" + (run* + q + (fresh + (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF) + (== c0 1) + (== c1 1) + (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)) + (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)))) + (list)) + +(mk-tests-run!)