1:- module(hamiton, []). 2
3:- use_module(zdd('zdd-array')). 4:- use_module(zdd(zdd)). 5:- use_module(pac(op)). 6 9
15
16hamilton(X, Y, Z):- udg_path_count(X, Y, Z).
17
19udg_path_count(Ends, Links, C):- udg_path_count(Ends, Links, C, _).
20
22udg_path_count(Ends, Links, C, X):-
23 prepare_udg(Ends, Links),
24 !,
25 get_key(coa, Coa),
26 udg_mate_prune(Coa, 1, X),
27 card(X, C).
29udg_mate_prune(Ls, X, Y):-
30 add_links(Ls, X, Y0), 31 get_key(ends, A-B),
32 prune_final(A, B, Y0, Y).
33
36
65
68
69rect_hamilton(R, C) :- rect_path_count(R, C).
71rect_path_count(R, C):- R = rect(W, H),
72 rect_path_count( p(0,0) - p(W,H), R, C).
74rect_path_count(Ends, R, C):- rect_links(R, Links),
75 udg_path_count(Ends, Links, C).
76
79rect_links(rect(W, H), Links):-
80 findall( p(I,J) - p(K,L),
81 ( between(0, W, I),
82 between(0, H, J),
83 ( L = J, K is I + 1, K =< W
84 ; K = I, L is J + 1, L =< H
85 )
86 ),
87 Links).
88
89 92
93
101
107
108prepare_udg(ST, Links):-
109 prepare_udg(Links),
110 prepare_ends(ST, A-B),
111 set_key(ends, A-B).
113prepare_udg(Links):-
114 prepare_udg(Links, Succs, D, Vec),
115 length(D, N),
116 completing_succs(Succs, Succs0, N),
117 set_key(coa, Succs0),
118 set_key(dom, D),
119 set_key(frontier, Vec).
121prepare_udg(Links, Succs, D, Vec):-
122 intern_links(Links, Links0),
123 normal_mate_list(Links0, Links1),
124 sort(Links1, Links2),
125 domain_of_links(Links2, D),
126 rel_to_fun(Links2, Succs),
127 Vec=..[#|D],
128 setup_frontier(Links1, Vec).
130prepare_ends(A-B, R):-!, R = A0-B0,
131 memo(node_id(A)-I),
132 memo(node_id(B)-J),
133 ( nonvar(I), nonvar(J) -> sort([I, J], [A0, B0])
134 ; format("No link at ~w or ~w\n", [A,B]),
135 fail
136 ).
137prepare_ends(E, _):-
138 format("Unexpected form of end nodes ~w \n", [E]),
139 fail.
140
143completing_succs(X, X, 0):-!.
144completing_succs([I-A|Ls], [I-A|Ms], I):-!, J is I - 1,
145 completing_succs(Ls, Ms, J).
146completing_succs(Ls, [I-[]|Ms], I):- J is I - 1,
147 completing_succs(Ls, Ms, J).
148
151normal_mate_list([], []).
152normal_mate_list([P|R], [P0|R0]):- P = I-J,
153 ( J @< I -> P0 = J - I
154 ; P0 = P
155 ),
156 normal_mate_list(R, R0).
166rel_to_fun(L, R):- sort(L, L0), rel_to_fun(L0, [], R).
168rel_to_fun([], X, X).
169rel_to_fun([A-B|L], [A-U|V], R):-!,
170 rel_to_fun(L, [A-[B|U]|V], R).
171rel_to_fun([A-B|L], U, R):-!,
172 rel_to_fun(L, [A-[B]|U], R).
173
175domain_of_links(X, Y):-
176 findall(A , ( member(L, X),
177 ( L = (A - _)
178 ; L = (_ - A)
179 )
180 ),
181 Y0),
182 sort(Y0, Y).
183
185node_id(N, C, C0):- node_id(N, _, C, C0).
186
189node_id(N, I, C, C0):- memo(node_id(N)-I),
190 ( nonvar(I) -> C0 = C
191 ; C0 is C+1,
192 I = C0
193 ).
194
197intern_links(L, L0):- intern_links(L, L0, 0, _).
199intern_links([], [], C, C).
200intern_links([A-B|L], [I-J|M], C, D):-
201 node_id(A, I, C, C0),
202 node_id(B, J, C0, C1),
203 intern_links(L, M, C1, D).
204
205
214on_frontier(I, J, F):- arg(I, F, K), K < J.
224
232
233
234
235off_frontier(I, J, F):- arg(I, F, K), K >= J.
236
238setup_frontier([], _).
239setup_frontier([I-J|L], F):-
240 update_frontier(I, J, F),
241 !,
242 setup_frontier(L, F).
243
246update_frontier(I, J, V):-
247 arg(J, V, A),
248 ( I < A -> setarg(J, V, I)
249 ; true
250 ).
251
252 255
258arrow_symbol( _ -> _).
260arrow_symbol(A, A0):- functor(A, A0, 2).
261arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2),
262 arg(1, A, A1),
263 arg(2, A, A2).
264
266composable_pairs(A-B, A-C, B, C).
267composable_pairs(A-B, C-A, B, C).
268composable_pairs(B-A, A-C, B, C).
269composable_pairs(B-A, C-A, B, C).
271normal_pair(A-B, B-A):- B < A, !.
272normal_pair(A->B, B->A):- B < A, !.
273normal_pair(X, X).
275strong_less_than(_-A, B-_):- A<B.
276
277 281add_links([], X, X):-!.
282add_links([A-Ns|Ls], X, Y):-!,
283 cofact(X0, t(A-A, 0, X)),
284 add_links(A, Ns, X0, X1),
285 prune_by_frontier(A, X1, X2),
286 add_links(Ls, X2, Y).
288add_links(_, [], X, X):-!.
289add_links(A, [B|Ns], X, Y):-
290 add_link(A-B, X, X0),
291 zdd_join(X, X0, X1),
292 add_links(A, Ns, X1, Y).
294add_link(_, X, 0):- X<2, !.
295add_link(U, X, Y):-
296 cofact(X, t(A, L, R)),
297 arrow_symbol(A, F),
298 ( F = (->) -> Y = 0
299 ; add_link(U, L, L0),
300 ( U = A -> R0 = 0
301 ; strong_less_than(U, A) -> R0 = 0
302 ; ( composable_pairs(U, A, V, W) ->
303 U = (Ul-Ur),
304 subst_node([Ul->Ur], V, W, R, R0)
305 ; add_link(U, R, R1),
306 zdd_insert(A, R1, R0)
307 )
308 ),
309 zdd_join(L0, R0, Y)
310 ).
312subst_node(_, _, _, X, 0):- X<2, !.
313subst_node(Es, A, P, X, Y):- cofact(X, t(U, L, R)), 314 arrow_symbol(U, F, Lu, Ru),
315 ( F = (->) -> Y = 0
316 ; subst_node(Es, A, P, L, L0),
317 ( Ru = A ->
318 normal_pair(Lu-P, V),
319 zdd_ord_insert([V|Es], R, R0)
320 ; Lu = A ->
321 normal_pair(P-Ru, V),
322 zdd_ord_insert([V|Es], R, R0)
323 ; subst_node(Es, A, P, R, R1),
324 zdd_insert(U, R1, R0)
325 ),
326 zdd_join(L0, R0, Y)
327 ).
328
329 332
333prune_by_frontier(I, X, Y):-
334 get_key(frontier, V),
335 get_key(ends, M),
336 prune_by_frontier(X, Y, I, M, V).
343prune_by_frontier(X, X, _, _, _):- X<2, !.
344prune_by_frontier(X, Y, I, M, V):- cofact(X, t(A, L, R)),
345 classify_pair(A, I, M, V, C),
346 ( C = arrow -> Y = X
347 ; prune_by_frontier(L, L0, I, M, V),
348 ( C = keep ->
349 prune_by_frontier(R, R1, I, M, V),
350 zdd_insert(A, R1, R0)
351 ; C = ignore ->
352 prune_by_frontier(R, R0, I, M, V)
353 ; R0 = 0
354 ),
355 zdd_join(L0, R0, Y)
356 ).
357
358
360on_pair(J, J-_).
361on_pair(J, _-J).
363classify_pair((_->_), _, _, _, arrow):-!.
364classify_pair(J-J, I, _, V, C):-!,
365 ( on_frontier(J, I, V) -> C = keep
366 ; C = 0
367 ).
368classify_pair(J-K, I, Pair, V, C):-
369 ( on_frontier(J, I, V) ->
370 ( on_frontier(K, I, V) -> C = keep
371 ; ( on_pair(K, Pair) -> C = keep
372 ; C = 0
373 )
374 )
375 ; on_pair(J, Pair)->
376 ( on_frontier(K, I, V) -> C = keep
377 ; on_pair(K, Pair) -> C = keep
378 ; C = 0
379 )
380 ; C = 0
381 ).
382
384prune_final(_, _, X, 0):- X<2, !.
385prune_final(P, Q, X, Y):- cofact(X, t(A, _L, R)),
386 ( A = (_->_) -> Y = 0
387 ; A = P-Q -> prune_final0(R, Y)
388 ; Y = 0
389 ).
391prune_final0(X, X):- X<2, !.
392prune_final0(X, Y):- cofact(X, t(A, _L, _R)),
393 ( A = (_->_) -> Y = X
394 ; Y = 0
395 )