From 2921aa30b43ebea7d9a41394af41970c12c39392 Mon Sep 17 00:00:00 2001 From: giles Date: Sat, 9 May 2026 14:06:47 +0000 Subject: [PATCH] =?UTF-8?q?mk:=20phase=206=20piece=20D=20=E2=80=94=20send-?= =?UTF-8?q?more-money=20+=20Sudoku=204x4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two CLP(FD) demo puzzles plus an underlying improvement. clpfd.sx: each fd-* posting goal now wraps its post-time propagation in fd-fire-store, so cross-constraint narrowing happens BEFORE labelling. Without this, a chain like fd-eq xyc z-plus-tenc1 followed by fd-plus 2 ten-c1 z-plus-tenc1 wouldn't deduce ten-c1 = 10 until labelling kicked in. Now the deduction happens at goal-construction time. Guard against (c s2) returning nil before fd-fire-store runs. tests/send-more-money.sx: full column-by-column carry encoding (D+E = Y+10*c1; N+R+c1 = E+10*c2; E+O+c2 = N+10*c3; S+M+c3 = O+10*M). Verifies the encoding against the known answer (9 5 6 7 1 0 8 2); the full search labelling 11 vars from {0..9} is too slow for naive labelling order — documented as a known limitation. Real CLP(FD) needs first-fail / failure-driven heuristics for SMM to be fast. tests/sudoku-4x4.sx: 16 cells / 12 distinctness constraints. The empty grid enumerates exactly 288 distinct fillings (the known count for 4x4 Latin squares with 2x2 box constraints). An impossible-clue test (two 1s in row 0) fails immediately. 50/50 sudoku + smm tests, full clpfd suite green at 132/132. --- lib/minikanren/clpfd.sx | 36 ++++++--- lib/minikanren/tests/send-more-money.sx | 97 +++++++++++++++++++++++++ lib/minikanren/tests/sudoku-4x4.sx | 89 +++++++++++++++++++++++ 3 files changed, 210 insertions(+), 12 deletions(-) create mode 100644 lib/minikanren/tests/send-more-money.sx create mode 100644 lib/minikanren/tests/sudoku-4x4.sx 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!)