fc+cdj works

csp/hacs-map.rkt

@@ -0,0 +1,58 @@
+#lang debug racket
+(require "hacs.rkt")
+(module+ test (require rackunit))
+
+(define (map-coloring-csp colors neighbors)
+  (define variables (remove-duplicates (flatten neighbors) eq?))
+  (define vds (for/list ([var (in-list variables)])
+                ($var var colors null)))
+  (define cs (for*/list ([neighbor neighbors]
+                         [target (cdr neighbor)])
+               ($constraint (list (car neighbor) target) neq?)))
+  ($csp vds cs))
+
+(define (parse-colors str) (map string->symbol (map string-downcase (regexp-match* "." str))))
+(define(parse-neighbors str)
+  (define recs (map string-trim (string-split str ";")))
+  (for/list ([rec recs])
+    (match-define (cons head tail) (string-split rec ":"))
+    (map string->symbol (map string-downcase (map string-trim (cons head (string-split (if (pair? tail)
+                                                                                           (car tail)
+                                                                                           ""))))))))
+  
+
+(current-inference forward-check)
+(current-select-variable minimum-remaining-values)
+(define aus (map-coloring-csp (parse-colors "RGB")
+                              (parse-neighbors "SA: WA NT Q NSW V; NT: WA Q; NSW: Q V; T: ")))
+
+(module+ test
+  (check-equal? (length (solve* aus)) 18))
+
+(define usa (map-coloring-csp (parse-colors "RGBY")
+                              (parse-neighbors "WA: OR ID; OR: ID NV CA; CA: NV AZ; NV: ID UT AZ; ID: MT WY UT;
+        UT: WY CO AZ; MT: ND SD WY; WY: SD NE CO; CO: NE KA OK NM; NM: OK TX;
+        ND: MN SD; SD: MN IA NE; NE: IA MO KA; KA: MO OK; OK: MO AR TX;
+        TX: AR LA; MN: WI IA; IA: WI IL MO; MO: IL KY TN AR; AR: MS TN LA;
+        LA: MS; WI: MI IL; IL: IN KY; IN: OH KY; MS: TN AL; AL: TN GA FL;
+        MI: OH IN; OH: PA WV KY; KY: WV VA TN; TN: VA NC GA; GA: NC SC FL;
+        PA: NY NJ DE MD WV; WV: MD VA; VA: MD DC NC; NC: SC; NY: VT MA CT NJ;
+        NJ: DE; DE: MD; MD: DC; VT: NH MA; MA: NH RI CT; CT: RI; ME: NH;
+        HI: ; AK:")))
+
+(module+ test
+  (check-true (pair? (solve usa))))
+
+(define fr (map-coloring-csp (parse-colors "RGBY")
+                             (parse-neighbors "AL: LO FC; AQ: MP LI PC; AU: LI CE BO RA LR MP; BO: CE IF CA FC RA
+        AU; BR: NB PL; CA: IF PI LO FC BO; CE: PL NB NH IF BO AU LI PC; FC: BO
+        CA LO AL RA; IF: NH PI CA BO CE; LI: PC CE AU MP AQ; LO: CA AL FC; LR:
+        MP AU RA PA; MP: AQ LI AU LR; NB: NH CE PL BR; NH: PI IF CE NB; NO:
+        PI; PA: LR RA; PC: PL CE LI AQ; PI: NH NO CA IF; PL: BR NB CE PC; RA:
+        AU BO FC PA LR")))
+
+(module+ test
+(check-true (pair? (solve fr))))
+
+(module+ main
+  (solve aus))

csp/hacs-smm.rkt

@@ -0,0 +1,47 @@
+#lang br
+(require "hacs.rkt")
+
+;  SEND
+;+ MORE
+;------
+; MONEY
+
+(define $vd +var)
+
+(define (word-value . xs)
+  (for/sum ([(x idx) (in-indexed (reverse xs))])
+    (* x (expt 10 idx))))
+
+(define vs '(s e n d m o r y))
+(define vds (for/list ([k vs])
+              ($vd k (range 10))))
+
+(define (not= x y) (not (= x y)))
+
+(define alldiffs
+  (for/list ([pr (in-combinations vs 2)])
+    ($constraint pr not=)))
+
+(define (smm-func s e n d m o r y)
+  (= (+ (word-value s e n d) (word-value m o r e)) (word-value m o n e y)))
+
+(define csp ($csp vds (append
+                           
+                           alldiffs
+                           (list
+                            ($constraint vs smm-func)
+                            ($constraint '(s) positive?)
+                            ($constraint '(m) (λ (x) (= 1 x)))
+                            ($constraint '(d e y) (λ (d e y) (= (modulo (+ d e) 10) y)))
+                            ($constraint '(n d r e y) (λ (n d r e y)
+                                                        (= (modulo (+ (word-value n d) (word-value r e)) 100)
+                                                           (word-value e y))))
+                            ($constraint '(e n d o r y) (λ (e n d o r y)
+                                                          (= (modulo (+ (word-value e n d) (word-value o r e)) 1000) (word-value n e y))))))))
+(parameterize ([current-select-variable mrv]
+               [current-order-values lcv]
+               [current-inference mac])
+  (time (solve csp)))
+(nassigns csp)
+(nchecks csp)
+(reset! csp)

csp/hacs-test.rkt

@@ -0,0 +1,71 @@
+#lang debug racket
+(require "hacs.rkt" rackunit)
+
+(check-equal? (first-unassigned-variable ($csp (list (+var 'a (range 3)) (+var 'b (range 3))) null))
+              (+var 'a (range 3)))
+(check-equal? (first-unassigned-variable ($csp (list (+avar 'a (range 3)) (+var 'b (range 3))) null))
+              (+var 'b (range 3)))
+(check-false (first-unassigned-variable ($csp (list (+avar 'a (range 3)) (+avar 'b (range 3))) null)))
+
+(check-equal?
+ ;; no forward checking when no constraints
+ ($csp-vars (forward-check ($csp (list (+avar 'a '(1)) (+var 'b (range 2))) null) 'a))
+ (list (+avar 'a '(1)) (+var 'b '(0 1))))
+
+(check-equal?
+ ($csp-vars (forward-check (forward-check ($csp (list (+avar 'a '(1))  (+avar 'b '(0)) (+var 'c '(0 1 2)))
+                                                (list ($constraint '(a c) (negate =))
+                                                      ($constraint '(b c) (negate =)))) 'a) 'b))
+ (list (+avar 'a '(1)) (+avar 'b '(0) '()) (+var 'c '(2) '(b a))))
+
+(check-equal?
+ ;; no inconsistency: b≠c not checked when fc is relative to a
+ ($csp-vars (forward-check ($csp (list (+avar 'a '(1))  (+var 'b (range 2)) (+var 'c '(0)))
+                                 (list ($constraint '(a b) (negate =))
+                                       ($constraint '(b c) (negate =)))) 'a))
+ (list (+avar 'a '(1)) (+var 'b '(0) '(a)) (+var 'c '(0))))
+
+(check-equal?
+ ;; no inconsistency: a≠b not checked when fc ignores a, which is already assigned
+ ($csp-vars (forward-check ($csp (list (+avar 'a '(1))  (+avar 'b '(1)) (+var 'c (range 2)))
+                                 (list ($constraint '(a b) (negate =))
+                                       ($constraint '(b c) (negate =)))) 'b))
+ (list (+avar 'a '(1)) (+avar 'b '(1)) (+var 'c '(0) '(b))))
+
+(check-exn $backtrack?
+           (λ () ($csp-vars (forward-check ($csp (list (+avar 'a '(1))
+                                                       (+var 'b '(1)))
+                                                 (list ($constraint '(a b) (negate =)))) 'a))))
+
+
+(check-equal? ($csp-vars (forward-check ($csp (list (+avar 'a (range 3))
+                                                    (+var 'b (range 3)))
+                                              (list ($constraint '(a b) <)
+                                                    ($constraint '(a b) <)
+                                                    ($constraint '(a b) <))) 'a))
+              (list (+avar 'a '(0 1 2)) (+var 'b '(1 2) '(a))))
+
+(check-equal?
+ (parameterize ([current-inference forward-check])
+   (length (solve* ($csp (list (+var 'x (range 3))
+                               (+var 'y (range 3))
+                               (+var 'z (range 3)))
+                         (list ($constraint '(x y) <>)
+                               ($constraint '(x z) <>)
+                               ($constraint '(y z) <>)))))) 6)
+
+(parameterize ([current-inference forward-check])
+  (define vds (for/list ([k '(wa nt nsw q t v sa)])
+                (+var k '(red green blue))))
+  (define cs (list
+              ($constraint '(wa nt) neq?)
+              ($constraint '(wa sa) neq?)
+              ($constraint '(nt sa) neq?)
+              ($constraint '(nt q) neq?)
+              ($constraint '(q sa) neq?)
+              ($constraint '(q nsw) neq?)
+              ($constraint '(nsw sa) neq?)
+              ($constraint '(nsw v) neq?)
+              ($constraint '(v sa) neq?)))
+  (define csp ($csp vds cs))
+  (check-equal? (length (solve* csp)) 18))

csp/hacs.rkt

@@ -1,27 +1,27 @@
 #lang debug racket
-(require racket/generator sugar graph rackunit math)
+(require racket/generator)
 (provide (all-defined-out))
 
 (struct $csp ([vars #:mutable]
               [constraints #:mutable]) #:transparent)
 (struct $constraint (names proc) #:transparent)
-(struct $var (name vals past conflicts) #:transparent)
-(define (+var name vals [past null] [conflicts null])
-  ($var name vals past conflicts))
+(struct $var (name domain past) #:transparent)
+(define (+var name vals [past null])
+  ($var name vals past))
   
 (define $var-name? symbol?)
 (struct $avar $var () #:transparent)
-(define (+avar name vals [past null] [conflicts null])
-  ($avar name vals past conflicts))
+(define (+avar name vals [past null])
+  ($avar name vals past))
 (struct inconsistency-signal (csp) #:transparent)
 
-(struct $conflict (names) #:transparent)
+(struct $backtrack (names) #:transparent)
 
 (define current-select-variable (make-parameter #f))
 (define current-order-values (make-parameter #f))
 (define current-inference (make-parameter #f))
 (define current-solver (make-parameter #f))
-
+(define current-shuffle (make-parameter #t))
 
 (define/contract (check-name-in-csp! caller csp name)
   (symbol? $csp? $var-name? . -> . void?)
@@ -39,7 +39,7 @@
 (define/contract ($csp-vals csp name)
   ($csp? $var-name? . -> . (listof any/c))
   (check-name-in-csp! '$csp-vals csp name)
-  ($var-vals ($csp-var csp name)))
+  ($var-domain ($csp-var csp name)))
 
 (define order-domain-values values)
 (define/contract (assign-val csp name val)
@@ -47,7 +47,7 @@
   ($csp
    (for/list ([var ($csp-vars csp)])
      (if (eq? name ($var-name var))
-         (+avar name (list val) ($var-past var) ($var-conflicts var))
+         (+avar name (list val) ($var-past var))
          var))
    ($csp-constraints csp)))
 
@@ -56,22 +56,34 @@
   ($csp
    (for/list ([var ($csp-vars csp)])
      (match var
-       [($var (? (λ (x) (eq? x name))) vals past _)
+       [($var (? (λ (x) (eq? x name))) vals past)
         (+avar name vals past conflicts)]
        [else var]))
    ($csp-constraints csp)))
 
+(define (unassigned-vars csp)
+  (for/list ([var (in-list ($csp-vars csp))]
+             #:unless ($avar? var))
+    var))
+
 (define/contract (first-unassigned-variable csp)
   ($csp? . -> . (or/c #false (and/c $var? (not/c $avar?))))
-  (for/first ([var (in-list ($csp-vars csp))]
-              #:unless ($avar? var))
-    var))
+  (match (unassigned-vars csp)
+    [(? empty?) #false]
+    [xs (first xs)]))
+
+(define/contract (argmin-random-tie proc xs)
+  (procedure? (non-empty-listof any/c) . -> . any/c)
+  (define ordered-xs (sort xs < #:key proc))
+  (first ((if (current-shuffle) shuffle values)
+          (takef ordered-xs (λ (x) (= (proc (car ordered-xs)) (proc x)))))))
 
-(check-equal? (first-unassigned-variable ($csp (list (+var 'a (range 3)) (+var 'b (range 3))) null))
-              (+var 'a (range 3)))
-(check-equal? (first-unassigned-variable ($csp (list (+avar 'a (range 3)) (+var 'b (range 3))) null))
-              (+var 'b (range 3)))
-(check-false (first-unassigned-variable ($csp (list (+avar 'a (range 3)) (+avar 'b (range 3))) null)))
+(define/contract (minimum-remaining-values csp)
+  ($csp? . -> . (or/c #false (and/c $var? (not/c $avar?))))
+  (struct $mrv-rec (var num) #:transparent)
+  (match (unassigned-vars csp)
+    [(? empty?) #false]
+    [xs (argmin-random-tie (λ (var) (length ($var-domain var))) xs)]))
 
 (define first-domain-value values)
 
@@ -88,109 +100,83 @@
 (define/contract (forward-check csp aname)
   ($csp? $var-name? . -> . $csp?)
   (define aval (first ($csp-vals csp aname)))
-  (define (filter-vals var)
-    (match-define ($var name vals past conflicts) var)
-    (match (($csp-constraints csp) . relating . (list aname name))
-      [(? empty?) var]
-      [constraints
-       (define new-vals
-         (for/list ([val (in-list vals)]
-                    #:when (for/and ([constraint (in-list constraints)])
-                             (let ([proc ($constraint-proc constraint)])
-                               (if (eq? name (first ($constraint-names constraint)))
-                                   (proc val aval)
-                                   (proc aval val)))))
-           val))
-       (unless (pair? new-vals)
-         (raise ($conflict past)))
-       (+var name new-vals (cons aname past) conflicts)]))
-
-  ($csp
-   (for/list ([var (in-list ($csp-vars csp))])
-     (if ($avar? var)
-         var
-         (filter-vals var)))
-   ($csp-constraints csp)))
-
-(check-equal?
- ;; no forward checking when no constraints
- ($csp-vars (forward-check ($csp (list (+avar 'a '(1)) (+var 'b (range 2))) null) 'a))
- (list (+avar 'a '(1)) (+var 'b '(0 1))))
-
-(check-equal?
- ($csp-vars (forward-check (forward-check ($csp (list (+avar 'a '(1))  (+avar 'b '(0)) (+var 'c '(0 1 2)))
-                                                (list ($constraint '(a c) (negate =))
-                                                      ($constraint '(b c) (negate =)))) 'a) 'b))
- (list (+avar 'a '(1)) (+avar 'b '(0) '()) (+var 'c '(2) '(b a))))
-
-(check-equal?
- ;; no inconsistency: b≠c not checked when fc is relative to a
- ($csp-vars (forward-check ($csp (list (+avar 'a '(1))  (+var 'b (range 2)) (+var 'c '(0)))
-                                 (list ($constraint '(a b) (negate =))
-                                       ($constraint '(b c) (negate =)))) 'a))
- (list (+avar 'a '(1)) (+var 'b '(0) '(a)) (+var 'c '(0))))
-
-(check-equal?
- ;; no inconsistency: a≠b not checked when fc ignores a, which is already assigned
- ($csp-vars (forward-check ($csp (list (+avar 'a '(1))  (+avar 'b '(1)) (+var 'c (range 2)))
-                                 (list ($constraint '(a b) (negate =))
-                                       ($constraint '(b c) (negate =)))) 'b))
- (list (+avar 'a '(1)) (+avar 'b '(1)) (+var 'c '(0) '(b))))
-
-(check-exn $conflict?
-           (λ () ($csp-vars (forward-check ($csp (list (+avar 'a '(1))
-                                                       (+var 'b '(1)))
-                                                 (list ($constraint '(a b) (negate =)))) 'a))))
-
-
-(check-equal? ($csp-vars (forward-check ($csp (list (+avar 'a (range 3))
-                                                    (+var 'b (range 3)))
-                                              (list ($constraint '(a b) <)
-                                                    ($constraint '(a b) <)
-                                                    ($constraint '(a b) <))) 'a))
-              (list (+avar 'a '(0 1 2)) (+var 'b '(1 2) '(a))))
-
+  (define (check-var var)
+    (match var
+      [(? $avar?) var]
+      [($var name vals past)
+       (match (($csp-constraints csp) . relating . (list aname name))
+         [(? empty?) var]
+         [constraints
+          (define new-vals
+            (for/list ([val (in-list vals)]
+                       #:when (for/and ([constraint (in-list constraints)])
+                                (let ([proc ($constraint-proc constraint)])
+                                  (if (eq? name (first ($constraint-names constraint)))
+                                      (proc val aval)
+                                      (proc aval val)))))
+              val))
+          (+var name new-vals (cons aname past))])]))
+  (define checked-vars (map check-var ($csp-vars csp)))
+  ;; conflict-set will be empty if there are no empty domains
+  (define conflict-set (for*/list ([var (in-list checked-vars)]
+                                   #:when (empty? ($var-domain var))
+                                   [name (in-list ($var-past var))])
+                         name))
+  ;; for conflict-directed backjumping it's essential to forward-check ALL vars
+  ;; (even after an empty domain is generated) and combine their conflicts
+  ;; so we can discover the *most recent past var* that could be the culprit.
+  ;; If we just bail out at the first conflict, we may backjump too far based on its history
+  ;; (and thereby miss parts of the search tree)
+  (when (pair? conflict-set)
+    (raise ($backtrack conflict-set)))
+  ($csp checked-vars ($csp-constraints csp)))
 
 (define/contract (backtracking-solver
                   csp
-                  #:select-variable [select-unassigned-variable (or (current-select-variable) first-unassigned-variable)]
+                  #:select-variable [select-unassigned-variable
+                                     (or (current-select-variable) first-unassigned-variable)]
                   #:order-values [order-domain-values (or (current-order-values) first-domain-value)]
                   #:inference [inference (or (current-inference) no-inference)])
   (($csp?) (#:select-variable procedure? #:order-values procedure? #:inference procedure?) . ->* . generator?)
   (generator ()
-             (let backtrack ([csp csp])
+             (let loop ([csp csp])
                (match (select-unassigned-variable csp)
                  [#false (yield csp)]
-                 [($var name vals _ _)
+                 [($var name domain _)
+                  (define (wants-backtrack? exn)
+                    (and ($backtrack? exn) (memq name ($backtrack-names exn))))
                   (for/fold ([conflicts null]
-                             #:result (void conflicts))
-                            ([val (in-list (order-domain-values vals))])
-                    (with-handlers ([$conflict?
-                                     (λ (c)
-                                       (match c
-                                         [($conflict names) (cond
-                                                              [(empty? names) conflicts]
-                                                              [(memq name names)
-                                                                (append conflicts (remq name names))]
-                                                              [else (raise c)])]))])
-                      (let* ([csp (assign-val csp name val)]
-                             [csp (inference csp name)])
-                        (backtrack csp))
-                      conflicts))]))))
+                             #:result (void))
+                            ([val (in-list (order-domain-values domain))])
+                    (with-handlers ([wants-backtrack?
+                                     (λ (bt) (append conflicts (remq name ($backtrack-names bt))))])
+                      (define csp-with-assignment (assign-val csp name val))
+                      (loop (inference csp-with-assignment name)))
+                    conflicts)]))))
+
+(define/contract (solution-consistent? solution)
+  ($csp? . -> . boolean?)
+  (for/and ([c (in-list ($csp-constraints solution))])
+    (apply ($constraint-proc c) (for*/list ([name (in-list ($constraint-names c))]
+                                            [var (in-list ($csp-vars solution))]
+                                            #:when (eq? name ($var-name var)))
+                                  (first ($var-domain var))))))
 
 (define/contract (solve* csp
                          #:finish-proc [finish-proc $csp-vars]
                          #:solver [solver (or (current-solver) backtracking-solver)]
                          #:count [max-solutions +inf.0])
-  (($csp?) (#:finish-proc procedure? #:solver generator? #:count integer?) . ->* . (listof any/c))
+  (($csp?) (#:finish-proc procedure? #:solver procedure? #:count integer?) . ->* . (listof any/c))
   (for/list ([solution (in-producer (solver csp) (void))]
              [idx (in-range max-solutions)])
+    (unless (solution-consistent? solution)
+      (raise (list 'wtf solution)))
     (finish-proc solution)))
 
 (define/contract (solve csp
                         #:finish-proc [finish-proc $csp-vars]
                         #:solver [solver (or (current-solver) backtracking-solver)])
-  (($csp?) (#:finish-proc procedure? #:solver generator?) . ->* . (or/c #false any/c))
+  (($csp?) (#:finish-proc procedure? #:solver procedure?) . ->* . (or/c #false any/c))
   (match (solve* csp #:finish-proc finish-proc #:solver solver #:count 1)
     [(list solution) solution]
     [else #false]))
@@ -198,27 +184,3 @@
 (define (<> a b) (not (= a b)))
 (define (neq? a b) (not (eq? a b)))
 
-(check-equal?
- (parameterize ([current-inference forward-check])
-   (length (solve* ($csp (list (+var 'x (range 3))
-                               (+var 'y (range 3))
-                               (+var 'z (range 3)))
-                         (list ($constraint '(x y) <>)
-                               ($constraint '(x z) <>)
-                               ($constraint '(y z) <>)))))) 6)
-
-(parameterize ([current-inference forward-check])
-    (define vds (for/list ([k '(wa nsw t q nt v sa)])
-                  (+var k '(red green blue))))
-    (define cs (list
-                ($constraint '(wa nt) neq?)
-                ($constraint '(wa sa) neq?)
-                ($constraint '(nt sa) neq?)
-                ($constraint '(nt q) neq?)
-                ($constraint '(q sa) neq?)
-                ($constraint '(q nsw) neq?)
-                ($constraint '(nsw sa) neq?)
-                ($constraint '(nsw v) neq?)
-                ($constraint '(v sa) neq?)))
-    (define csp ($csp vds cs))
-    (check-equal? (time (length (solve* csp))) 18))