DFS operators for minikanren

Here we have the usual minikanren fair search operators

and then modified "depth first" variants

This allows mk programming where you can select which kind search subprograms should use

(define-syntax conj+
  (syntax-rules ()
    ((_ g) (Zzz g))
    ((_ g0 g ...) (conj (Zzz g0) (conj+ g ...)))))

(define-syntax disj+
  (syntax-rules ()
    ((_ g) (Zzz g))
    ((_ g0 g ...) (disj (Zzz g0) (disj+ g ...)))))

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...))))

;; depth first search versions of the same

(define-syntax conj+/dfs
  (syntax-rules ()
    ((_ g) g)
    ((_ g0 g ...) (conj/dfs g0 (conj+/dfs g ...)))))

(define-syntax disj+/dfs
  (syntax-rules ()
    ((_ g) g)
    ((_ g0 g ...) (disj/dfs g0 (disj+/dfs g ...)))))

(define-syntax conde/dfs
  (syntax-rules ()
    ((_ (g0 g ...) ...) (disj+/dfs (conj+ g0 g ...) ...))))

The difference is simply that we don't "delay" using Zzz in the DFS version.








Canada

How can we represent a map in minikanren? A list of the regions and then as association list explaining what each region is next to.

becomes

(define nodes
  '(quebec
    northwest-territories
    ontario
    british-columbia
    manitoba
    alberta
    saskatchewan
    yukon
    nunavut
    newfoundland-and-labrador
    new-brunswick
    nova-scotia
    prince-edward-island))

(define edges
  '((quebec ontario)
    (quebec new-brunswick)
    (quebec newfoundland-and-labrador)
    (northwest-territories yukon)
    (northwest-territories british-columbia)
    (northwest-territories alberta)
    (northwest-territories saskatchewan)
    (northwest-territories nunavut)
    (ontario manitoba)
    (british-columbia yukon)
    (british-columbia alberta)
    (manitoba saskatchewan)
    (manitoba nunavut)
    (alberta saskatchewan)
    (new-brunswick nova-scotia)))







The solver in mk

Here is the minikanren code for coloring in these maps!

The function "graph-good-ordering" (omitted from this slide) is what does the map reduction in order to figure out how to arrange the minikanren program so that it only uses local backtracking. That is just a pure scheme function with no minikanren or unification involved.

(define (coloro x)
  (membero x '(red green blue yellow)))

(define (different-colors table)
  (lambda (constraint)
    (fresh (x y x-color y-color)
      (== constraint `(,x ,y))
      (assoco x table x-color)
      (assoco y table y-color)
      (=/= x-color y-color))))

(define (my-mapo p l i)
  ;; This has to be done in a depth first search!
  ;; (display (make-list i '-)) (newline)
  (conde/dfs ((== l '()))
	     ((fresh/dfs (car cdr)
		(== l `(,car . ,cdr))
		(p car)
		(my-mapo p cdr (+ i 1))))))

(define (color states edges colors)
  ;; This is a simple constrained generate and test solver
  ;; The interesting part was the graph reduction preprocessing
  ;; stage.
  (fresh (table)
    ;; make a list to hold the color of each state
    (make-assoc-tableo states colors table)
    
    ;; make sure each color is different to neighbours
    (mapo (different-colors table) edges)
    
    ;; brute force search for a valid coloring
    (my-mapo coloro colors 0)))

(define (do-australia)
  (let ((nodes (graph-good-ordering australia:nodes australia:edges)))
    (run^ 1 (lambda (q) (color nodes australia:edges q)))))

(define (do-canada)
  (let ((nodes (graph-good-ordering canada:nodes canada:edges)))
    (run^ 1 (lambda (q) (color nodes canada:edges q)))))

(define (do-america)
  (let ((nodes (graph-good-ordering america:nodes america:edges)))
    (run^ 1 (lambda (q) (color nodes america:edges q)))))







Results!

Using DFS to solve these map coloring problems give a huge speedup!

Without DFS

With DFS