1:- module(frtvec2, [udg_path_count/3, 2 udg_path_count/4, 3 rect_path_count/4, 4 rect_links/2, 5 udg_path/2 6 ]). 7 8:- use_module(zdd('zdd-array')). 9:- use_module(zdd(zdd)). 10:- use_module(pac(op)). 11:- use_module(zdd('prepare-udg')). 12 13 14% ?- zdd. 15% ?- N = 6, complete_udg(N, Links), udg_path_count(1-N, Links, C). 16% ?- N = 6, 17% complete_udg(N, Links), 18% forall((between(1, N, I), K is I + 1, between(K, N, J)), 19% udg_path_count(I-J, Links, C)). 20 21complete_udg(N, Links):- N>=2, 22 findall(I-J, 23 ( between(1, N, I), 24 K is I + 1, 25 between(K, N, J) 26 ), 27 Links). 28 29 30% ?- zdd. 31% ?- paths_of_complete_graph(2, X), card(X, C). 32%@ X = 2, 33%@ C = 1. 34% ?- paths_of_complete_graph(3, X), card(X, C). 35%@ X = 5, 36%@ C = 2. 37% ?- paths_of_complete_graph(4, X), card(X, C). 38%@ X = 19, 39%@ C = 5. 40% ?- paths_of_complete_graph(5, X), card(X, C). 41%@ X = 66, 42%@ C = 16. 43% ?- time((paths_of_complete_graph(10, X), card(X, C))). 44%@ % 2,330,986 inferences, 0.328 CPU in 0.406 seconds (81% CPU, 7106556 Lips) 45%@ X = 22574, 46%@ C = 109601. 47% ?- time((paths_of_complete_graph(11, X), card(X, C))). 48%@ % 7,972,033 inferences, 0.787 CPU in 0.811 seconds (97% CPU, 10130420 Lips) 49%@ X = 75638, 50%@ C = 986410. 51%@ % 7,972,199 inferences, 0.872 CPU in 1.035 seconds (84% CPU, 9145734 Lips) 52%@ X = 75638, 53%@ C = 986410. 54% ?- time((paths_of_complete_graph(12, X), card(X, C))). 55%@ % 26,995,652 inferences, 3.237 CPU in 3.792 seconds (85% CPU, 8338858 Lips) 56%@ X = 252547, 57%@ C = 9864101. 58% ?- time((paths_of_complete_graph(13, X), card(X, C))). 59%@ % 92,585,306 inferences, 10.461 CPU in 12.055 seconds (87% CPU, 8850663 Lips) 60%@ X = 839844, 61%@ C = 108505112. 62% ?- time((paths_of_complete_graph(14, X), card(X, C))). 63%@ % 283,495,642 inferences, 37.943 CPU in 43.815 seconds (87% CPU, 7471541 Lips) 64%@ X = 2783757, 65%@ C = 1302061345. 66% ?- time((paths_of_complete_graph(15, X), card(X, C))). 67%@ % 969,329,257 inferences, 139.219 CPU in 158.912 seconds (88% CPU, 6962626 Lips) 68%@ X = 9214955, 69%@ C = 16926797486. 70 71 72paths_of_complete_graph(2, X):-!, zdd_singleton(1-2, X). 73paths_of_complete_graph(N, X):- N>2, 74 N0 is N - 1, 75 paths_of_complete_graph(N0, Y), 76 add_new_node(N, Y, Z), 77 zdd_join(Y, Z, X). 78% 79add_new_node(_, X, 0):- X<2, !. 80add_new_node(N, X, Y):- memo(insnode(N, X)-Y), 81 ( nonvar(Y) -> true %, write(.) % many hits. 82 ; cofact(X, t(A, L, R)), 83 add_new_node(N, L, L0), 84 A = I-J, 85 zdd_ord_insert([I-N, J-N], R, R0), 86 add_new_node(N, R, R1), 87 zdd_insert(A, R1, R2), 88 zdd_join_list([L0, R0, R2], Y) 89 ). 90 91 92 93% ?- zdd. 94% ?- num_of_paths_in_complete_graph_by_zdd(3, C). 95% ?- num_of_paths_in_complete_graph_by_zdd(10, C). 96%@ C = 109601. 97% ?- num_of_paths_in_complete_graph_by_zdd(12, C). 98%@ C = 9864101. 99 100 101num_of_paths_in_complete_graph_by_zdd(N, C):- 102 complete_udg(N, Links), 103 udg_path_count(1-N, Links, C). 104 105% 224,373,208 inferences, 27.201 CPU in 31.332 seconds (87% CPU, 8248747 Lips 106 107% ?- N = 10, complete_udg(N, Links), 108% time(udg_path_count(1-N, Links, C)), 109% num_of_paths_in_complete_graph(N, C0), 110% compare(Comp, C, C0). 111%@ % 224,373,208 inferences, 27.201 CPU in 31.332 seconds (87% CPU, 8248747 Lips) 112%@ N = 10, 113%@ Links = [1-2, 1-3, 1-4, 1-5, 1-6, 1-7, 1-8, 1-9, ... - ...|...], 114%@ C = C0, C0 = 109601, 115%@ Comp = (=) . 116 117% ?- N = 11, complete_udg(N, Links), 118% time(udg_path_count(1-N, Links, C)), 119% num_of_paths_in_complete_graph(N, C0), 120% compare(Comp, C, C0). 121%@ % 1,122,834,167 inferences, 141.880 CPU in 162.471 seconds (87% CPU, 7913988 Lips) 122%@ N = 11, 123%@ Links = [1-2, 1-3, 1-4, 1-5, 1-6, 1-7, 1-8, 1-9, ... - ...|...], 124%@ C = C0, C0 = 986410, 125%@ Comp = (=) . 126 127% ?- num_of_paths_in_complete_graph(2, P). 128% ?- num_of_paths_in_complete_graph(3, P). 129% ?- num_of_paths_in_complete_graph(4, P). 130% ?- num_of_paths_in_complete_graph(5, P). 131% ?- num_of_paths_in_complete_graph(6, P). 132% ?- num_of_paths_in_complete_graph(10, P). 133% ?- num_of_paths_in_complete_graph(12, P). 134% ?- num_of_paths_in_complete_graph(100, P). 135 136% ?- all_mono([a,b],[1,2], X), card(X, R). 137% ?- all_mono([a,b],[1,2,3], X), card(X, R). 138num_of_paths_in_complete_graph(2, 1):-!. 139num_of_paths_in_complete_graph(N, P):- N0 is N -2, 140 math:factorial(N0, F), 141 num_of_paths_in_complete_graph(0, N0, F, 1, P). 142% 143num_of_paths_in_complete_graph(I, N, _, P, P):- I>= N, !. 144num_of_paths_in_complete_graph(I, N, F, P0, P):- 145 math:factorial(I, F0), 146 P1 is F//F0 + P0, 147 J is I + 1, 148 num_of_paths_in_complete_graph(J, N, F, P1, P). 149 150% 151udg_path(ST, PathSet):- b_getval(coa, Coa), 152 b_setval(st, ST), 153 udg_mate_prune(Coa, 1, PathSet). 154 155 156% ?- ord_insert(a, [], R). 157% ?- ord_insert(a, [a,c], R). 158% ?- ord_insert(d, [b,c], R). 159ord_insert(X, [], [X]):-!. 160ord_insert(X, [Y|R], Z):- compare(C, X, Y), 161 ( C = (<) -> Z = [X, Y|R] 162 ; C = (=) -> Z = [Y|R] 163 ; ord_insert(X, R, Z0), 164 Z = [Y|Z0] 165 ). 166 167% ?- zdd. 168% ?- count_paths_in_comp_udg(2, C). 169% ?- count_paths_in_comp_udg(3, C). 170% ?- count_paths_in_comp_udg(4, C). 171% ?- count_paths_in_comp_udg(5, C). 172% ?- count_paths_in_comp_udg(10, C). 173% ?- time(count_paths_in_comp_udg(12, C)). 174%@ % 61,408,802 inferences, 5.956 CPU in 7.545 seconds (79% CPU, 10310346 Lips) 175%@ C = 9864101 . 176% ?- time(count_paths_in_comp_udg(13, C)). 177%@ % 727,235,629 inferences, 76.901 CPU in 85.308 seconds (90% CPU, 9456730 Lips)% 727,235,629 inferences, 82.690 CPU in 93.161 seconds (89% CPU, 8794723 Lips) 178%@ C = 108505112 . 179%@ C = 108505112 . 180% ?- call_with_time_limit(160, time(count_paths_in_comp_udg(14, C))). 181%@ % 1,618,867,619 inferences, 264.140 CPU in 330.791 seconds (80% CPU, 6128827 Lips) 182%@ ERROR: Unhandled exception: Time limit exceeded 183 184 185% ?- count_paths_in_comp_udg(20, C). 186 187% ?- num_of_paths_in_complete_graph(6, P). 188% ?- num_of_paths_in_complete_graph(10, P). 189% ?- num_of_paths_in_complete_graph(20, P). 190% ?- num_of_paths_in_complete_graph(100, P). 191 192count_paths_in_comp_udg(N, C):- paths_in_comp_udg(N, Paths), 193 length(Paths, C). 194 195% ?- zdd. 196% ?- paths_in_comp_udg(2, R). 197% ?- paths_in_comp_udg(3, R). 198% ?- paths_in_comp_udg(4, R), maplist(writeln, R). 199 200 201paths_in_comp_udg(2, [[1-2]]). 202paths_in_comp_udg(N, Ps):- N>2, 203 N0 is N - 1, 204 paths_in_comp_udg(N0, P0s), 205 insert_node(N, P0s, P0s, Ps). 206 207% :- table insert_node/4. 208insert_node(_, [], Ps, Ps):-!. 209insert_node(K, [P|R], P0s, Ps):- 210 insert_node_to_path(K, [], P, P0s, P1s), 211 insert_node(K, R, P1s, Ps). 212 213insert_node_to_path(_, _, [], Ps, Ps):-!. 214insert_node_to_path(K, Q, [I-J|P], P0s, Ps):- 215 math:reverse(Q, [I-K,J-K|P], P0), 216 insert_node_to_path(K, [I-J|Q], P, [P0|P0s], Ps). 217 218 219% 1x1 1, 220% 2x2 2, 221% 3x3 12, 222% 4x4 184, 223% 5x5 8512, 224% 6x6 1262816, 225% 7x7 575780564, 226% 8x8 789360053252, 227% 9x9 3266598486981642, 228% 10x10 41044208702632496804, 229% 11x11 1568758030464750013214100, 230% 12x12 182413291514248049241470885236, 231% 13x13 64528039343270018963357185158482118, 232% ----------------------------------------------------- 233% 14x14 69450664761521361664274701548907358996488 234 235 /****************************** 236 * counting path in UDG * 237 ******************************/ 238 239% ?- zdd. 240% ?- trace. 241% ?- udg_path_count(a*d, [a-b, b-c, c-d], C). % fail. 242% ?- udg_path_count(a-x, [a-b, b-c, c-d], C). % fail. 243% ?- udg_path_count(a-b, [a-b], C, X), psa(X). 244% ?- udg_path_count(a-b, [a-b], C). 245 246% ?- udg_path_count(a-d, [a-b, b-c, c-d], C, X), psa(X). 247% ?- udg_path_count(a-c, [a-b, b-c, a-d, d-c], C, X), psa(X). 248 249 250% ?- listing(open_state). 251% ?- N = 11, findall(I-J, ( between(1, N, I), between(1, N, J), I < J), Ls), 252% time(zdd udg_path_count(1-N, Ls, C)). 253%@ % 1,835,060,694 inferences, 233.677 CPU in 238.492 seconds (98% CPU, 7852993 Lips) 254%@ N = 11, 255%@ Ls = [1-2, 1-3, 1-4, 1-5, 1-6, 1-7, 1-8, 1-9, ... - ...|...], 256%@ C = 986410. 257 258% [2024/01/04] Is global variable efficient ? 259% ?- N = 11, findall(I-J, ( between(1, N, I), between(1, N, J), I < J), Ls), 260% time(zdd udg_path_count(1-N, Ls, C)). 261%@ % 1,775,162,524 inferences, 211.846 CPU in 216.653 seconds (98% CPU, 8379506 Lips) 262%@ N = 11, 263%@ Ls = [1-2, 1-3, 1-4, 1-5, 1-6, 1-7, 1-8, 1-9, ... - ...|...], 264%@ C = 986410. 265% 266udg_path_count(Ends, Links, C):- udg_path_count(Ends, Links, C, _). 267 268% 269udg_path_count(Ends, Links, C, X):- 270 prepare_udg_reverse(Ends, Links), 271 !, 272 b_getval(st, ST), 273 b_getval(frontier, Vec), 274 b_setval(efr, efr(ST, Vec)), 275 b_getval(coa, Coa), 276% show_udg, 277% writeln(st=ST), 278 udg_mate_prune(Coa, 1, X), 279 card(X, C). 280 281% 282udg_mate_prune(Ls, X, Y):- 283 add_links(Ls, X, Y0), 284 b_getval(st, ST), 285 prune_final(ST, Y0, Y). 286 287 288% ?- zdd. 289% ?- time((rect_path_count(p(0,0)-p(1,1), rect(1,1), C, _))). 290% ?- time((rect_path_count(p(0,0)-p(2,2), rect(2,2), C, _))). 291% ?- time((rect_path_count(p(3,3)-p(4,4), rect(6,6), C, _))). 292% ?- time((rect_path_count(p(0,0)-p(6,6), rect(6,6), C, _))). 293% ?- time(rect_path_count(rect(1,0), C)). 294% ?- time(rect_path_count(rect(1,1), C)). 295% ?- time(rect_path_count(rect(2,1), C)). 296% ?- time(rect_path_count(rect(1,3), C)). 297% ?- time(rect_path_count(rect(3,1), C)). 298% ?- time(rect_path_count(rect(4,1), C)). 299% ?- time(rect_path_count(rect(5,1), C)). 300% ?- time(rect_path_count(rect(2,2), C)). 301% ?- udg_path_count(a-i, [a-b, a-d, b-e, b-c, d-e, d-g, e-f, c-h, 302% f-i, g-h, h-i], C, X), psa(X). 303% ?- time(rect_path_count(rect(3,3), C)). 304%@ % 834,404 inferences, 0.194 CPU in 0.210 seconds (92% CPU, 4309960 Lips) 305%@ C = 184. 306% ?- time(rect_path_count(rect(4,4), C, X)). 307%@ % 4,668,538 inferences, 0.429 CPU in 0.515 seconds (83% CPU, 10883464 Lips) 308%@ C = 8512, 309%@ X = 1022. 310 311% ?- profile(time(rect_path_count(rect(5,5), C))). 312%@ % 24,473,932 inferences, 2.897 CPU in 2.982 seconds (97% CPU, 8447665 Lips) 313%@ C = 1262816. 314%@ % 24,472,015 inferences, 2.648 CPU in 3.331 seconds (80% CPU, 9240675 Lips) 315%@ C = 1262816. 316 317% ?- time(rect_path_count(rect(6,6), C)). 318%@ % 129,512,904 inferences, 12.272 CPU in 14.575 seconds (84% CPU, 10553524 Lips) 319%@ C = 575780564. 320 321% ?- time(rect_path_count(rect(7,7), C)). 322% imac [2025/06/08] 323%@ % 644,164,539 inferences, 66.242 CPU in 77.915 seconds (85% CPU, 9724483 Lips) 324%@ C = 789360053252. 325 326% ?- time(rect_path_count(rect(8,8), C)). 327%@ % 3,191,842,013 inferences, 359.074 CPU in 417.936 seconds (86% CPU, 8889098 Lips) 328%@ C = 3266598486981642. 329 330% ?- time(rect_path_count(rect(9,9), C)). 331%@ done 332%@ % 12,641,494,607 inferences, 3374.703 CPU in 3619.570 seconds (93% CPU, 3745958 Lips) 333%@ C = 41044208702632496804. 334 335% ?- time(rect_path_count(rect(9,9), C)). 336%@ % 12,584,483,532 inferences, 1528.588 CPU in 1775.464 seconds (86% CPU, 8232752 Lips) 337%@ C = 41044208702632496804. 338 339% ?- time(rect_path_count(rect(10,10), C)). 340%@ % 59,632,082,303 inferences, 7437.316 CPU in 8649.928 seconds (86% CPU, 8017958 Lips) 341%@ C = 1568758030464750013214100. 342 343% ?- zdd. 344% MBP[2025/05/25] 345% ?- time(rect_path_count(rect(10,10), C)). 346%@ % 73,969,583,595 inferences, 10031.989 CPU in 10198.439 seconds (98% CPU, 7373371 Lips) 347%@ C = 1568758030464750013214100 348 349 350% ?- time(rect_path_count(rect(11,11), C)). 351%@ % 277,342,057,605 inferences, 35622.993 CPU in 41124.669 seconds (87% CPU, 7785479 Lips) 352%@ C = 182413291514248049241470885236. 353 354% [2024/09/03] 13 x 13 grid graph passed also by the simple frontier vector. 355% ?- time(rect_path_count(rect(12,12), C)). 356% 1,273,378,663,129 inferences, 176187.026 CPU in 244597.424 seconds (72% CPU, 7227426 Lips) 357% C = 64528039343270018963357185158482118. 358 359% ?- C = 182413291514248049241470885236, 360% C1 = 64528039343270018963357185158482118, 361% D is C1//C. 362%@ C = 182413291514248049241470885236, 363%@ C1 = 64528039343270018963357185158482118, 364%@ D = 353746. 365 366% ?- X is 176187//3600. 367%@ X = 48. 368 369 370% ?- forall(between(1, 13, I), (X is 2^(I*I), writeln(I=> X))). 371rect_path_count(R, C):- rect_path_count(R, C, _). 372% 373rect_path_count(R, C, X):- 374 R = rect(W, H), 375 rect_path_count( p(0,0) - p(W,H), R, C, X). 376% 377rect_path_count(Pair, R, C, X):- rect_links(R, Links), 378 udg_path_count(Pair, Links, C, X). 379 380 381 /******************************** 382 * Prepare UDG in coalgebra * 383 ********************************/
390% ?- X=f(1,2,3), setup_frontier([1-2,2-3], X), on_frontier(1, 3, X). 391on_frontier(I, J, F):- arg(I, F, K), K @=< J. 392 393 /******************* 394 * Helpers * 395 *******************/ 396 397% ?- arrow_symbol(_->_, F). 398% ?- arrow_symbol(a->b, F, X, Y). 399arrow_symbol( _ -> _). 400% 401arrow_symbol(A, A0):- functor(A, A0, 2). 402arrow_symbol(A, A0, A1, A2):- functor(A, A0, 2), 403 arg(1, A, A1), 404 arg(2, A, A2). 405 406 /************************ 407 * core predicates * 408 ************************/ 409 410add_links([], X, X):-!. 411add_links([A-Ns|Ls], X, Y):- 412 b_getval(efr, EF), 413 writeln(node(A)), 414 prune_by_frontier(EF, A, X, X0), 415 bdd_cons(X1, A-A, X0), 416 add_links(A, Ns, X1, X2), 417 slim_gc(X2, X3), 418 add_links(Ls, X3, Y). 419% 420add_links(_, [], X, X):-!. 421add_links(A, [B|Ns], X, Y):- 422 b_getval(st, ST), 423 add_link(A-B, X, X0, ST), 424 zdd_join(X, X0, X1), 425 add_links(A, Ns, X1, Y). 426% 427add_link(_, X, 0, _):- X<2, !. 428add_link(U, X, Y, ST):- % memo useless here. 429 cofact(X, t(A, L, R)), 430 add_link(U, L, L0, ST), 431 U = (U1 - U2), 432 arrow_symbol(A, F, A1, A2), 433 ( F = (->) -> R0 = 0 434 ; U = A -> R0 = 0 % cycle found 435 ; U2 @< A1 -> R0 = 0 436 ; ( U1 = A1 -> 437 ( on_pair(A1, ST), A1\==A2 -> R0 = 0 438 ; subst_node(U1 -> U2, U2, A2, R, R0) 439 ) 440 ; U2 = A1 -> 441 ( on_pair(A1, ST), A1\==A2 -> R0 = 0 442 ; subst_node(U1 -> U2, U1, A2, R, R0) 443 ) 444 ; U2 = A2 -> 445 ( on_pair(A2, ST), A1\==A2 -> R0 = 0 446 ; subst_node(U1 -> U2, U1, A1, R, R0) 447 ) 448 ; add_link(U, R, R1, ST), 449 zdd_insert(A, R1, R0) 450 ) 451 ), 452 zdd_join(L0, R0, Y). 453 454% 455subst_node(_, _, _, X, 0):- X<2, !. 456subst_node(E, A, P, X, Y):- % memo useless here 457 cofact(X, t(U, L, R)), 458 subst_node(E, A, P, L, L0), % replace A with P 459 arrow_symbol(U, F, Lu, Ru), 460 ( F = (->) -> R0 = 0 461 ; Ru = A -> 462 normal_pair(Lu - P, V), 463 zdd_ord_insert([V, E], R, R0) 464 ; Lu = A -> 465 normal_pair(P - Ru, V), 466 zdd_ord_insert([V, E], R, R0) 467 ; A @< Lu -> R0 = 0 468 ; subst_node(E, A, P, R, R1), 469 zdd_insert(U, R1, R0) 470 ), 471 zdd_join(L0, R0, Y). 472 473 474 /*************************** 475 * Prune by frontier * 476 ***************************/
488prune_by_frontier(_, _, X, X):- X < 2, !. 489prune_by_frontier(EF, I, X, Y):- cofact(X, t(A, L, R)), 490 EF = efr(ST, V), 491 ( A = (_->_) -> Y = X 492 ; prune_by_frontier(EF, I, L, L0), 493 classify_pair(A, I, ST, V, C), 494 ( C = arrow -> zdd_insert(A, R, R0) 495 ; C = keep -> 496 prune_by_frontier(EF, I, R, R1), 497 zdd_insert(A, R1, R0) 498 ; C = ignore -> 499 prune_by_frontier(EF, I, R, R0) 500 ; R0 = 0 501 ), 502 zdd_join(L0, R0, Y) 503 ). 504 505 506% works! [2024/01/11] 507classify_pair(J-J, I, ST, V, C):-!, 508 ( on_frontier(J, I, V) -> C = keep 509 ; on_pair(J, ST) -> C = 0 510 ; C = ignore 511 ). 512classify_pair(J-K, I, ST, V, C):- % J\==K. 513 ( on_frontier(J, I, V) -> 514 ( on_frontier(K, I, V) -> C = keep 515 ; on_pair(K, ST) -> C = keep 516 ; C = 0 517 ) 518 ; on_frontier(K, I, V) -> 519 ( on_pair(J, ST) -> C = keep 520 ; C = 0 521 ) 522 ; C = 0 523 ). 524 525% ?- zdd. 526% ?- X<< {[1-6,2-2,5-5,(1->3),(3->4),(4->6)]}, 527% prune_final(1-6, X, Y), psa(Y). 528 529% ?- X<< +[*[a-b, a->b]], prune_final(a-b, X, Y), psa(X), psa(Y). 530prune_final(_, X, 0):- X < 2, !. 531prune_final(Pair, X, Y):- cofact(X, t(A, L, R)), 532 prune_final(Pair, L, L0), 533 ( A = (_->_) -> R0 = 0, writeln('unexpected ***arrow***') 534 ; A = Pair -> prune_final0(R, R0) 535 ; A = V-V -> prune_final(Pair, R, R0) 536 ; R0 = 0 537 ), 538 zdd_join(L0, R0, Y). 539% 540prune_final0(X, X):- X < 2, !. 541prune_final0(X, Y):- cofact(X, t(A, L, R)), 542 ( A = (_->_) -> Y = X 543 ; prune_final0(L, L0), 544 ( A = (V - V) -> prune_final0(R, R0) 545 ; R0 = 0 546 ) 547 ), 548 zdd_join(L0, R0, Y)