debug instrumenting

main
Matthew Butterick 6 years ago
parent a33946cc48
commit 7f557f0f01

@ -1,5 +1,5 @@
#lang debug racket
(require "hacs.rkt" rackunit sugar/list)
(require "hacs.rkt" rackunit sugar/list sugar/debug)
(current-inference forward-check)
(current-select-variable mrv-degree-hybrid)
@ -59,7 +59,7 @@
(parameterize ([current-inference forward-check])
(define vds (for/list ([k '(wa nt nsw q t v sa)])
($var k '(red green blue))))
($var k '(red green blue))))
(define cs (list
($constraint '(wa nt) neq?)
($constraint '(wa sa) neq?)
@ -78,7 +78,7 @@
(add-vars! quarters '(dollars quarters) (range 26))
(add-constraint! quarters (λ (d q) (= 26 (+ d q))) '(dollars quarters))
(add-constraint! quarters (λ (d q) (= 17 (+ d (* 0.25 q)))) '(dollars quarters))
(check-equal? (time (solve quarters))
(check-equal? (time-named (solve quarters))
'((dollars . 14) (quarters . 12)))
@ -102,7 +102,7 @@
(add-constraint! xsum (λ (r1 r2 r3 r4 x) (= 27 (+ r1 r2 r3 r4 x))) '(r1 r2 r3 r4 x))
(add-pairwise-constraint! xsum alldiff= '(l1 l2 l3 l4 r1 r2 r3 r4 x))
(check-equal? (length (time (solve* xsum))) 8)
(check-equal? (length (time-named (solve* xsum))) 8)
@ -119,7 +119,7 @@
(define (word-value . xs)
(for/sum ([(x idx) (in-indexed (reverse xs))])
(* x (expt 10 idx))))
(* x (expt 10 idx))))
(define smm (make-csp))
(add-vars! smm '(s e n d m o r y) (λ () (range 10)))
@ -136,7 +136,7 @@
(word-value m o n e y))) '(s e n d m o r y))
(add-pairwise-constraint! smm alldiff= '(s e n d m o r y))
(check-equal? (parameterize ([current-select-variable mrv-degree-hybrid]) ; todo: why is plain mrv so bad on this problem?
(time (solve smm))) '((s . 9) (e . 5) (n . 6) (d . 7) (m . 1) (o . 0) (r . 8) (y . 2)))
(time-named (solve smm))) '((s . 9) (e . 5) (n . 6) (d . 7) (m . 1) (o . 0) (r . 8) (y . 2)))
;; queens problem
@ -147,19 +147,19 @@
(add-vars! queens qs rows)
(define (q-col q) (string->number (string-trim (symbol->string q) "q")))
(for* ([qs (in-combinations qs 2)])
(match-define (list qa qb) qs)
(match-define (list qa-col qb-col) (map q-col qs))
(add-constraint! queens
(λ (qa-row qb-row)
(and
(not (= (abs (- qa-row qb-row)) (abs (- qa-col qb-col)))) ; same diagonal?
(not (= qa-row qb-row)))) ; same row?
(list qa qb)))
(match-define (list qa qb) qs)
(match-define (list qa-col qb-col) (map q-col qs))
(add-constraint! queens
(λ (qa-row qb-row)
(and
(not (= (abs (- qa-row qb-row)) (abs (- qa-col qb-col)))) ; same diagonal?
(not (= qa-row qb-row)))) ; same row?
(list qa qb)))
(check-equal? 92 (length (time (solve* queens))))
(check-equal? 92 (length (time-named (solve* queens))))
#;(parameterize ([current-solver min-conflicts])
(solve queens))
(solve queens))
#|
@ -208,14 +208,14 @@
(add-vars! zebra ps '(dogs snails foxes horses zebra))
(for ([vars (list ns cs ds ss ps)])
(add-pairwise-constraint! zebra neq? vars))
(add-pairwise-constraint! zebra neq? vars))
(define (paired-with lval left rval right)
(add-constraint! zebra (λ (left right) (or (not (eq? left lval)) (eq? rval right))) (list left right)))
(define (paired-with* lval lefts rval rights)
(for ([left lefts][right rights])
(paired-with lval left rval right)))
(paired-with lval left rval right)))
;# 1. The englishman lives in a red house.
('englishman ns . paired-with* . 'red cs)
@ -250,13 +250,13 @@
(for ([righta (drop-right rights 2)]
[left (cdr lefts)]
[rightb (drop rights 2)])
(add-constraint! zebra (λ (left righta rightb)
(or (not (eq? left lval)) (eq? righta rval) (eq? rval rightb)))
(list left righta rightb)))
(add-constraint! zebra (λ (left righta rightb)
(or (not (eq? left lval)) (eq? righta rval) (eq? rval rightb)))
(list left righta rightb)))
(for ([left (list (first lefts) (last lefts))]
[right (list (second rights) (fourth rights))])
(add-constraint! zebra (λ (left right) (or (not (eq? left lval)) (eq? rval right)))
(list left right))))
(add-constraint! zebra (λ (left right) (or (not (eq? left lval)) (eq? rval right)))
(list left right))))
;# 10. The man who smokes chesterfields lives next to the one who keeps foxes.
('chesterfields ss . next-to . 'foxes ps)
@ -281,9 +281,19 @@
(check-equal? (parameterize ([current-select-variable mrv]
[current-shuffle #f])
(finish (time (solve zebra))))
(finish (time-named (solve zebra))))
'(((nationality-0 . norwegian) (color-0 . yellow) (drink-0 . water) (smoke-0 . kools) (pet-0 . foxes))
((nationality-1 . ukrainian) (color-1 . blue) (drink-1 . tea) (smoke-1 . chesterfields) (pet-1 . horses))
((nationality-2 . englishman) (color-2 . red) (drink-2 . milk) (smoke-2 . oldgold) (pet-2 . snails))
((nationality-3 . japanese) (color-3 . green) (drink-3 . coffee) (smoke-3 . parliaments) (pet-3 . zebra))
((nationality-4 . spaniard) (color-4 . ivory) (drink-4 . orange-juice) (smoke-4 . luckystrike) (pet-4 . dogs))))
(module+ main
(when-debug
(define-syntax n (λ (stx) #'10))
(time-avg n (void (solve quarters)))
(time-avg n (void (solve* xsum)))
(time-avg n (void (solve smm)))
(time-avg n (void (solve* queens)))
(time-avg n (void (solve zebra)))))

@ -2,16 +2,27 @@
(require racket/generator graph)
(provide (all-defined-out))
(define-syntax when-debug
(let ()
(define debug #f)
(if debug
(make-rename-transformer #'begin)
(λ (stx) (syntax-case stx ()
[(_ . rest) #'(void)])))))
(define-syntax-rule (in-cartesian x)
(in-generator (let ([argss x])
(let loop ([argss argss][acc empty])
(if (null? argss)
(yield (reverse acc))
(for ([arg (in-list (car argss))])
(loop (cdr argss) (cons arg acc))))))))
(loop (cdr argss) (cons arg acc))))))))
(struct $csp ([vars #:mutable]
[constraints #:mutable]) #:transparent)
(struct $csp (vars
constraints
[assignments #:auto]
[checks #:auto]) #:mutable #:transparent
#:auto-value 0)
(define csp? $csp?)
(define vars $csp-vars)
(define constraints $csp-constraints)
@ -25,7 +36,7 @@
(raise-argument-error '$constraint-proc "$csp" csp))
;; apply proc in many-to-many style
(for/and ([args (in-cartesian (map (λ (cname) ($csp-vals csp cname)) ($constraint-names constraint)))])
(apply ($constraint-proc constraint) args))))
(apply ($constraint-proc constraint) args))))
(define (make-constraint [names null] [proc values])
($constraint names proc))
@ -80,11 +91,11 @@
((csp? procedure? (listof (listof name?))) ((or/c #false name?)) . ->* . void?)
(set-$csp-constraints! csp (append (constraints csp)
(for/list ([names (in-list namess)])
(for ([name (in-list names)])
(check-name-in-csp! 'add-constraints! csp name))
(make-constraint names (if proc-name
(procedure-rename proc proc-name)
proc))))))
(for ([name (in-list names)])
(check-name-in-csp! 'add-constraints! csp name))
(make-constraint names (if proc-name
(procedure-rename proc proc-name)
proc))))))
(define/contract (add-pairwise-constraint! csp proc var-names [proc-name #false])
((csp? procedure? (listof name?)) (name?) . ->* . void?)
@ -118,7 +129,7 @@
(check-name-in-csp! 'csp-var csp name)
(for/first ([var (in-vars csp)]
#:when (eq? name (var-name var)))
var))
var))
(define/contract ($csp-vals csp name)
(csp? name? . -> . (listof any/c))
@ -131,7 +142,7 @@
(csp? name? . -> . any/c)
(for/or ([var (in-vars csp)]
#:when (assigned-var? var))
(eq? name (var-name var))))
(eq? name (var-name var))))
(define (reduce-function-arity proc pattern)
(unless (match (procedure-arity proc)
@ -162,27 +173,30 @@
(ormap assigned-name? ($constraint-names constraint)))
(make-csp (vars csp)
(for/list ([constraint (in-constraints csp)])
(cond
[(and (if minimum-arity (<= minimum-arity (constraint-arity constraint)) #true)
(partially-assigned? constraint))
(match-define ($constraint cnames proc) constraint)
($constraint (filter-not assigned-name? cnames)
;; pattern is mix of values and boxed symbols (indicating variables to persist)
;; use boxes here as cheap way to distinguish id symbols from value symbols
(let ([reduce-arity-pattern (for/list ([cname (in-list cnames)])
(if (assigned-name? cname)
(first ($csp-vals csp cname))
(box cname)))])
(reduce-function-arity proc reduce-arity-pattern)))]
[else constraint])))))
(cond
[(and (if minimum-arity (<= minimum-arity (constraint-arity constraint)) #true)
(partially-assigned? constraint))
(match-define ($constraint cnames proc) constraint)
($constraint (filter-not assigned-name? cnames)
;; pattern is mix of values and boxed symbols (indicating variables to persist)
;; use boxes here as cheap way to distinguish id symbols from value symbols
(let ([reduce-arity-pattern (for/list ([cname (in-list cnames)])
(if (assigned-name? cname)
(first ($csp-vals csp cname))
(box cname)))])
(reduce-function-arity proc reduce-arity-pattern)))]
[else constraint])))))
(define nassns 0)
(define (reset-assns!) (set! nassns 0))
(define/contract (assign-val csp name val)
(csp? name? any/c . -> . csp?)
(when-debug (set! nassns (add1 nassns)))
(make-csp
(for/list ([var (vars csp)])
(if (eq? name (var-name var))
($avar name (list val))
var))
(if (eq? name (var-name var))
($avar name (list val))
var))
(constraints csp)))
(define/contract (unassigned-vars csp)
@ -214,7 +228,7 @@
(csp? $var? . -> . exact-nonnegative-integer?)
(for/sum ([constraint (in-constraints csp)]
#:when (memq (var-name var) ($constraint-names constraint)))
1))
1))
(define/contract (blended-variable-selector csp)
(csp? . -> . (or/c #false (and/c $var? (not/c assigned-var?))))
@ -256,8 +270,8 @@
[cnames (in-value ($constraint-names constraint))]
#:when (and (= (length names) (length cnames))
(for/and ([name (in-list names)])
(memq name cnames))))
constraint))
(memq name cnames))))
constraint))
(define (binary-constraint? constraint)
(= 2 (constraint-arity constraint)))
@ -265,6 +279,9 @@
(define (constraint-relates? constraint name)
(memq name ($constraint-names constraint)))
(define nfchecks 0)
(define (reset-nfcs!) (set! nfchecks 0))
(define/contract (forward-check csp aname)
(csp? name? . -> . csp?)
(define aval (first ($csp-vals csp aname)))
@ -280,20 +297,21 @@
(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))
(let ([proc ($constraint-proc constraint)])
(if (eq? name (first ($constraint-names constraint)))
(proc val aval)
(proc aval val)))))
val))
($cvar name new-vals (cons aname (if ($cvar? var)
($cvar-past var)
null)))])]))
(define checked-vars (map check-var (vars csp)))
(when-debug (set! nfchecks (+ (length checked-vars) nchecks)))
;; 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 ($cvar-past var))])
name))
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.
@ -310,13 +328,13 @@
(constraint-relates? constraint aname)
(let ([other-name (first (remq aname ($constraint-names constraint)))])
(singleton-var? (csp-var csp other-name)))))
constraint))
constraint))
(make-csp checked-vars nonsingleton-constraints))
(define/contract (constraint-checkable? c names)
($constraint? (listof name?) . -> . any/c)
(for/and ([cname (in-list ($constraint-names c))])
(memq cname names)))
(memq cname names)))
(define/contract (constraint-arity constraint)
($constraint? . -> . exact-nonnegative-integer?)
@ -325,6 +343,8 @@
(define (singleton-var? var)
(= 1 (length ($var-domain var))))
(define nchecks 0)
(define (reset-nchecks!) (set! nchecks 0))
(define/contract (check-constraints csp)
(csp? . -> . csp?)
;; this time, we're not limited to assigned variables
@ -332,12 +352,13 @@
;; we also want to use "singleton" vars (that is, vars that have been reduced to a single domain value by forward checking)
(define singleton-varnames (for/list ([var (in-vars csp)]
#:when (singleton-var? var))
(var-name var)))
(var-name var)))
(define-values (checkable-constraints other-constraints)
(partition (λ (c) (constraint-checkable? c singleton-varnames)) (constraints csp)))
(for ([constraint (in-list (sort checkable-constraints < #:key constraint-arity))]
(for ([(constraint idx) (in-indexed (sort checkable-constraints < #:key constraint-arity))]
#:unless (constraint csp))
(backtrack!))
(when-debug (set! nchecks (+ (add1 idx) nchecks)))
(backtrack!))
;; discard checked constraints, since they have no further reason to live
(make-csp (vars csp) other-constraints))
@ -346,15 +367,15 @@
;; todo: why does this function slow down searches?
(make-csp
(for/list ([var (in-vars csp)])
(match-define ($var name vals) var)
(define procs (for*/list ([constraint (in-constraints csp)]
[cnames (in-value ($constraint-names constraint))]
#:when (and (= 1 (length cnames)) (eq? name (car cnames))))
($constraint-proc constraint)))
($var name
(for*/fold ([vals vals])
([proc (in-list procs)])
(filter proc vals))))
(match-define ($var name vals) var)
(define procs (for*/list ([constraint (in-constraints csp)]
[cnames (in-value ($constraint-names constraint))]
#:when (and (= 1 (length cnames)) (eq? name (car cnames))))
($constraint-proc constraint)))
($var name
(for*/fold ([vals vals])
([proc (in-list procs)])
(filter proc vals))))
(constraints csp)))
(define/contract (backtracking-solver
@ -388,23 +409,27 @@
;; todo: min-conflicts solver
(define/contract ($csp-assocs csp)
(define/contract (csp->assocs csp)
(csp? . -> . (listof (cons/c name? any/c)))
(for/list ([var (in-vars csp)])
(match var
[($var name domain) (cons name (first domain))])))
(match var
[($var name domain) (cons name (first domain))])))
(define/contract (solve* csp
#:finish-proc [finish-proc $csp-assocs]
#:finish-proc [finish-proc csp->assocs]
#:solver [solver (or (current-solver) backtracking-solver)]
#:count [max-solutions +inf.0])
((csp?) (#:finish-proc procedure? #:solver procedure? #:count integer?) . ->* . (listof any/c))
(when-debug
(reset-assns!)
(reset-nfcs!)
(reset-nchecks!))
(for/list ([solution (in-producer (solver csp) (void))]
[idx (in-range max-solutions)])
(finish-proc solution)))
(finish-proc solution)))
(define/contract (solve csp
#:finish-proc [finish-proc $csp-assocs]
#:finish-proc [finish-proc csp->assocs]
#:solver [solver (or (current-solver) backtracking-solver)])
((csp?) (#:finish-proc procedure? #:solver procedure?) . ->* . (or/c #false any/c))
(match (solve* csp #:finish-proc finish-proc #:solver solver #:count 1)

Loading…
Cancel
Save