diff --git a/csp/hacs-map.rkt b/csp/hacs-map.rkt new file mode 100644 index 00000000..f843dafc --- /dev/null +++ b/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)) \ No newline at end of file diff --git a/csp/hacs-smm.rkt b/csp/hacs-smm.rkt new file mode 100644 index 00000000..58e9ac67 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/csp/hacs-test.rkt b/csp/hacs-test.rkt new file mode 100644 index 00000000..94f2aad3 --- /dev/null +++ b/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)) \ No newline at end of file diff --git a/csp/hacs.rkt b/csp/hacs.rkt index 6cb8d28e..210bc391 100644 --- a/csp/hacs.rkt +++ b/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)) \ No newline at end of file