1:- module(zdd_samples, [ 2 ]). 3 4:- use_module(library(apply)). 5:- use_module(library(apply_macros)). 6:- use_module(library(clpfd)). 7:- use_module(library(statistics)). 8:- use_module(zdd('zdd-array')). 9:- use_module(util(math)). 10:- use_module(util(meta2)). 11:- use_module(pac(basic)). 12:- use_module(pac(meta)). 13:- use_module(util(misc)). 14:- use_module(pac('expand-pac')). % For the kind block. 15:- use_module(zdd('zdd-misc')). 16:- use_module(zdd(zdd)). 17:- use_module(pac(op)). 18 19:- set_prolog_flag(stack_limit, 10_200_147_483_648). 20% :- use_module(zdd('zdd-misc')). 21% :- use_module(zdd('zdd-graphviz')). 22% :- use_module(zdd('zdd-euler')). 23% :- use_module(zdd('zdd-reset-shift')). 24attr_unify_hook(V, Y):- 25 ( get_attr(Y, zdd, A) 26 -> zdd_unify(V, A) 27 ; zdd_unify(V, Y) 28 ). 29 30 :- op(1060, xfy, ~). % equivalence 31 :- op(1060, xfy, #). % exor 32 :- op(1060, xfy, <->). % equivalence 33 :- op(1050, yfx, <-). 34 :- op(1060, xfy, <=> ). % equivalence 35 :- op(1040, xfy, \/). % OR 36 :- op(1030, xfy, /\). % AND 37 :- op(1020, fy, \). % NOT 38 :- op(700, xfx, :=). % Assignment 39 :- op(1000, xfy, &). 40 41 42% for pac query. 43 :- pac:op(1000, xfy, &). 44 :- pac:op(700, xfx, :=). 45 46term_expansion --> pac:expand_pac. 47 48% ?- zdd((P<<pow([1,2,3]), use_zdd(fibo_with_memo(10, Fibo)))). 49% ?- zdd(zdd(zdd(fibo_with_memo(100, F)))). 50%@ F = 354224848179261915075 . 51% ?- time(zdd(use_zdd(fibo_with_memo(10000, F)))). 52%@ % 633,519 inferences, 0.057 CPU in 0.062 seconds (92% CPU, 11169235 Lips) 53%@ % 575,144 inferences, 0.057 CPU in 0.063 seconds (91% CPU, 10036716 Lips) 54 55fibo_with_memo(0, 0):-!. 56fibo_with_memo(1, 1):-!. 57fibo_with_memo(N, F):- memo(N-F), 58 ( nonvar(F) -> true 59 ; N0 is N-1, 60 N1 is N-2, 61 fibo_with_memo(N0, F0), 62 fibo_with_memo(N1, F1), 63 F is F0 + F1 64 ). 65 66% ?- open_state(S), fibo_with_memo(10000, X, S). 67 68% ?- open_state(S), time(fibo_with_memo(100, X, S)). 69%@ % 3,444 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 16400000 Lips) 70%@ S = .., 71%@ X = 354224848179261915075. 72% ?- open_state(S), time(fibo_with_memo(10000, _X, S)). 73%@ % 367,930 inferences, 2.168 CPU in 4.010 seconds (54% CPU, 169735 Lips) 74%@ S = .. . 75 76fibo_with_memo(0, 0, _):-!. 77fibo_with_memo(1, 1, _):-!. 78fibo_with_memo(N, F, S):- memo(N-F, S), 79 ( nonvar(F) -> true 80 ; N0 is N-1, 81 N1 is N-2, 82 fibo_with_memo(N0, F0, S), 83 fibo_with_memo(N1, F1, S), 84 F is F0 + F1 85 ). 86 87% ?- fibo_with_hash(0, Fibo). 88% ?- fibo_with_hash(1, Fibo). 89% ?- fibo_with_hash(2, Fibo). 90% ?- fibo_with_hash(3, Fibo). 91% ?- fibo_with_hash(10, Fibo). 92% ?- fibo_with_hash(100, Fibo). 93% ?- time(fibo_with_hash(1000, Fibo)). 94%@ % 30,515 inferences, 0.003 CPU in 0.003 seconds (87% CPU, 11314423 Lips) 95% ?- time(fibo_with_hash(10000, Fibo)). 96%@ % 347,954 inferences, 0.050 CPU in 0.072 seconds (69% CPU, 6981000 Lips) 97 98 99fibo_with_hash(N, F):- open_hash(2, H), 100 fibo_with_hash(N, F, H), 101 close_hash(H). 102% 103fibo_with_hash(0, 1, H):-!, hash(0, H, 1). 104fibo_with_hash(1, 1, H):-!, hash(1, H, 1). 105fibo_with_hash(N, F, H):- hash(N, H, F), 106 ( nonvar(F) -> true 107 ; N0 is N-1, 108 N1 is N-2, 109 fibo_with_hash(N0, F0, H), 110 fibo_with_hash(N1, F1, H), 111 F is F0 + F1 112 ). 113 114% ?- time(fast_fibo(10000, F)). 115%@ % 20,000 inferences, 0.018 CPU in 0.032 seconds (58% CPU, 1096852 Lips) 116% ?- time(fast_fibo(20000, F)). 117%@ % 39,999 inferences, 0.024 CPU in 0.039 seconds (63% CPU, 1637894 Lips) 118 119fast_fibo(N, F):- fast_fibo(N, _, _, F). 120% 121fast_fibo(0, 0, 0, 0):-!. 122fast_fibo(1, 0, 0, 1):-!. 123fast_fibo(N, X, Y, F):- N0 is N-1, 124 fast_fibo(N0, Y, _, X), 125 F is X + Y. 126 127% ?- zdd((P<<pow([1,2,3]), use_zdd(fibo_with_memo(100, Fibo), 1280), card(P,C))). 128%% fibonacci(+N, -F) is de<t. 129% Unify F with the value of the Fibonacci function for N. 130% :-table naive_fibo/2. 131% ?- time(naive_fibo(10, F)). 132% ?- call_with_time_limit(60, naive_fibo(1000, _)). 133%@ ERROR: Unhandled exception: Time limit exceeded <== without table. 134% ?- time(use_zdd(fibo_with_memo(1000, X))). 135%@ % 51,652 inferences, 0.005 CPU in 0.005 seconds (93% CPU, 10338671 Lips) 136% ?- time(use_zdd(fibo_with_memo(10000, X))). 137%@ % 573,228 inferences, 0.054 CPU in 0.058 seconds (92% CPU, 10662525 Lips) 138% ?- time(naive_fibo(1000, _)). 139% ?- time(naive_fibo(10000, _)). 140% ?- time(naive_fibo(100 000, _)). 141 142:- table naive_fibo/2. 143naive_fibo(0, 0):-!. 144naive_fibo(1, 1):-!. 145naive_fibo(X, S):- X0 is X-1, 146 X1 is X0-1, 147 naive_fibo(X0, S0), 148 naive_fibo(X1, S1), 149 S is S0 + S1. 150 151 /****************** 152 * N-queens * 153 ******************/ 154 155% ?- time(zdd(n_queens(8, C))). 156% ?- time(zdd(n_queens(9, C))). 157% ?- time(zdd(n_queens(10, C))). 158% ?- time(zdd(n_queens(11, C))). 159%@ % 11,708,109 inferences, 1.087 CPU in 1.103 seconds (99% CPU, 10769276 Lips) 160%@ C = 2680 . 161% ?- time(zdd(n_queens(12, C))). % [2021/04/21] 162%@ % 61,028,680 inferences, 6.153 CPU in 6.217 seconds (99% CPU, 9918445 Lips) 163%@ C = 14200 . 164 165% ?- time(zdd(n_queens(12, C))). % [2020/10/16] 166%@ % 60,919,433 inferences, 5.954 CPU in 5.968 seconds (100% CPU, 10232153 Lips) 167%@ C = 14200 . 168%@ % 11,708,109 inferences, 1.087 CPU in 1.103 seconds (99% CPU, 10769276 Lips) 169%@ C = 2680 . 170% ?- profile(zdd(n_queens(12, C))). % [2018/10/25] 171%@ C = 14200. 172% ?- time(zdd(n_queens(12, C))). % [2018/11/04] 173%@ % 54,199,597 inferences, 6.360 CPU 174%@ C = 14200 . 175% ?- time(zdd(n_queens(13, C))). % [2021/04/21] 176%@ % 352,183,186 inferences, 37.683 CPU in 37.882 seconds (99% CPU, 9345887 Lips) 177%@ C = 73712 . 178 179% ?- time(zdd(n_queens(13, C))). % [2018/11/01] 180%@ % 288,612,429 inferences, 36.548 CPU 181% ?- time(zdd(n_queens(14, C))). % [2018/10/25] 182%@ % 1,743,638,761 inferences, 256.849 CPU 183%@ C = 365596 . 184% ?- time(zdd(n_queens(14, C))). % [2020/10/16] 185%@ % 2,003,469,945 inferences, 221.555 CPU in 223.231 seconds (99% CPU, 9042752 Lips) 186%@ C = 365596 .
191n_queens(N, Count):- @(n_queens(N, Count)). 192 193n_queens(N, Count, State):- n_queen_matrix(N, M), 194 n_queens(M, [], [], [], S, State), 195 card(S, Count, State). 196% 197n_queens([], _, _, _, 1, _). 198n_queens([C|R], Po, Ne, Ho, U, S):- 199 n_queens(C, R, Po, Ne, Ho, U, S). 200 201% 202n_queens([], _, _, _, _, 0, _). 203n_queens([_I-J|D], R, Po, Ne, Ho, U, S):- memberchk(J, Ho), !, 204 n_queens(D, R, Po, Ne, Ho, U, S). 205n_queens([I-J|D], R, Po, Ne, Ho, U, S):- K is I+J, L is I-J, 206 ( check_safe(K, L, Po, Ne) 207 -> n_queens(R, [K|Po], [L|Ne], [J|Ho], V, S), 208 zdd_insert(K-L, V, V0, S), 209 n_queens(D, R, Po, Ne, Ho, U0, S), 210 zdd_join(V0, U0, U, S) 211 ; n_queens(D, R, Po, Ne, Ho, U, S) 212 ). 213 214% ?- matrix([1,2],[a,b], C). 215% ?- matrix([1,2],[], C). 216% ?- matrix([],[a,b], C).
220matrix(X, Y, Z):- matrix(X, Y, Z, []). 221% 222matrix([], _, L, L). 223matrix([A|As], Bs, [C|L], M):- 224 matrix(Bs, A, C, []), 225 matrix(As, Bs, L, M). 226% 227matrix([], _, L, L). 228matrix([B|Bs], A, [A-B|L], M):- matrix(Bs, A, L, M). 229 230% ?- n_queen_matrix(10, M). 231n_queen_matrix(N, M):- N0 is N-1, 232 numlist(0, N0, L), 233 matrix(L, L, M). 234% 235check_safe(K, L, Po, Ne):- 236 ( (memberchk(K, Po); memberchk(L, Ne)) 237 -> false 238 ; true 239 )