-
Notifications
You must be signed in to change notification settings - Fork 8
/
kcoloring.scm
81 lines (73 loc) · 1.99 KB
/
kcoloring.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
;; http://www.dmi.unipg.it/~formis/papers/JETAI07.pdf
;; p. 7
;; problem in CLP(FD)
;; (1) coloring(K, Vars) :-
;; (2) graph(Nodes, Edges),length(Nodes,N),
;; (3) length(Vars,N),
;; (4) domain(Vars, 1, K),
;; (5) constraints(Edges, Nodes, Vars),
;; (6) labeling([ff], Vars).
;; (7) constraints([],_,_).
;; (8) constraints([[A,B]|R], Nodes, Vars) :-
;; (9) nth(IdfA,Nodes,A),nth(IdfA,Vars,ColA),
;; (10) nth(IdfB,Nodes,B),nth(IdfB,Vars,ColB),
;; (11) ColA #\= ColB,
;; (12) constraints(R, Nodes, Vars).
;;
;; graph([1,2,3],[[1,2],[1,3],[2,3]]),
(define (grapho nodes edges)
(fresh ()
(== nodes '(1 2 3))
(== edges '((1 2) (1 3) (2 3)))))
(define (coloringo k vars)
(fresh (nodes edges n)
(grapho nodes edges)
(lengtho nodes n)
(lengtho vars n)
(for-eacho vars
(lambda (v)
(fresh ()
(z/assert `(<= 1 ,v))
(z/assert `(<= ,v ,k)))))
(constraintso edges nodes vars)
))
(define (constraintso edges nodes vars)
(conde
((== edges '()))
((fresh (a b r idfa idfb cola colb)
(== edges `((,a ,b) . ,r))
(=/= cola colb) (z/assert `(not (= ,cola ,colb)))
(ntho idfa nodes a) (ntho idfa vars cola)
(ntho idfb nodes b) (ntho idfb vars colb)
(constraintso r nodes vars)))))
(define (ntho i xs x)
(fresh (y ys)
(== `(,y . ,ys) xs)
(conde
((== i 0) (z/assert `(= ,i 0))
(== y x))
((=/= i 0)
(fresh (i-1)
(z/assert `(= ,i (+ ,i-1 1)))
(ntho i-1 ys x))))))
(define (for-eacho vars ro)
(conde
((== vars '()))
((fresh (x rest)
(== `(,x . ,rest) vars)
(ro x)
(for-eacho rest ro)))))
(define (lengtho xs n)
(fresh ()
(z/assert `(>= ,n 0))
(conde
((== xs '()) (== n 0) (z/assert `(= ,n 0)))
((fresh (x rest n-1)
(== `(,x . ,rest) xs)
(z/assert `(= ,n (+ ,n-1 1)))
(lengtho rest n-1))))))
;; non-deterministic result :(
#;
(test "3coloring"
(run* (q) (coloringo 3 q))
'((3 2 1) (3 1 2) (2 3 1) (1 3 2) (1 2 3) (2 1 3)))