Here is a favorite query sample on zdd programming. It works
for a set Ns of cardinality 10000 to enumarate the power set of Ns.
I’s fast enough, I think.
% ?-N = 10000, numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:= 2^N.
%@ % 1,298,553 inferences, 0.105 CPU in 0.114 seconds (92% CPU, 12364110 Lips)
%@ N = 10000,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = 10001.
As I dropped shit/reset control from my implementation of library(zdd),
I thought tabling should work on library(zdd). However, with the favorite sample above, query with tabling version was aborted with "not enough resources" even for a smaller set of 1000 elements.
% ?- numlist(1, 1000, Ns), (zdd X<<pow(Ns), card(X, C)).
%@ ERROR: '$tbl_variant_table'/6: Not enough resources: private_table_space
%@ ^ Exception: (11,771) catch('$tabling':create_table(<trie>(0x6000009a91e0), fresh(105553147668960, 105553129533248), ret(_78667858, _78417278, _78417280, _78417282, _78417284, _78417286, _78417288, _78417290, _78417292, _78417294, _78417296, _78417298, _78417300, _78417302, _78417304, _78417306, _78417308, _78417310, _78417312, _78417314, _78417316, _78417318, _78417320, _78417322, _78227762, _78227764, _78227766, _78227768, _78452420, _78452422, _78452424, _78452426), zmod:card_with_memo(22, _78667858, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(22, _78667858, s(..), s(..)))), deadlock, '$tabling':restart_tabling(<closure>(zmod:card_with_memo/4), zmod:card_with_memo(22, _78667858, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(22, _78667858, s(..), s(..))))) ? creep
%@ ^ Exception: (11,759) catch('$tabling':create_table(<trie>(0x6000009a9130), fresh(105553147668880, 105553129533104), ret(_78667638, _78417278, _78417280, _78417282, _78417284, _78417286, _78417288, _78417290, _78417292, _78417294, _78417296, _78417298, _78417300, _78417302, _78417304, _78417306, _78417308, _78417310, _78417312, _78417314, _78417316, _78417318, _78417320, _78417322, _78227762, _78227764, _78227766, _78227768, _78452420, _78452422, _78452424, _78452426), zmod:card_with_memo(23, _78667638, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(23, _78667638, s(..), s(..)))), deadlock, '$tabling':restart_tabling(<closure>(zmod:card_with_memo/4), zmod:card_with_memo(23, _78667638, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(23, _78667638, s(..), s(..))))) ? abort
%@ % Execution Aborted
The source codes are listed below. I guess ‘not enough resources’ was due to large argument S of zdd_join/4
and likely also for others. Usually S is a big term including vector and hash tables which are
extented to that of doubled size iteratively. S keeps every information
for computation. However, as for zdd programming, S is mainly to keep the functional dependency. So S should be safely ignored as for tabling, I think.
There might be already described in the documntation how to control
tabling for such card/3 and zdd_join/4, though I have failed to find.
source code with tabling or memo
:- table zdd_join/4.
%
zdd_join(0, X, X, _):-!.
zdd_join(X, 0, X, _):-!.
zdd_join(X, X, X, _):-!.
zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, Y, Z, S):-
cofact(X, t(A, L, R), S),
cofact(Y, t(A0, L0, R0), S),
zdd_compare(C, A, A0, S),
( C = (<) ->
zdd_join(L, Y, U, S),
cofact(Z, t(A, U, R), S)
; C = (=) ->
zdd_join(L, L0, U, S),
zdd_join(R, R0, V, S),
cofact(Z, t(A, U, V), S)
; zdd_join(L0, X, U, S),
cofact(Z, t(A0, U, R0), S)
).
%
card(X, Y, S):- setup_call_cleanup(
open_state(M),
card_with_memo(X, Y, S, M),
close_state(M)).
:- table card_with_memo/4.
card_with_memo(I, I, _, _):- I < 2, !.
card_with_memo(I, C, S, M):- % memo(I-C, M),
cofact(I, t(_, L, R), S),
card_with_memo(R, Cr, S, M),
card_with_memo(L, Cl, S, M),
C is Cl + Cr.
Default: zdd_join/4, card/3 without tabling but with memo.
zdd_join(0, X, X, _):-!.
zdd_join(X, 0, X, _):-!.
zdd_join(X, X, X, _):-!.
zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, Y, Z, S):-
( X@<Y -> memo(zdd_join(X,Y)-Z, S)
; memo(zdd_join(Y, X)-Z, S)
),
( nonvar(Z) -> true %, write(.)
; cofact(X, t(A, L, R), S),
cofact(Y, t(A0, L0, R0), S),
zdd_compare(C, A, A0, S),
( C = (<) ->
zdd_join(L, Y, U, S),
cofact(Z, t(A, U, R), S)
; C = (=) ->
zdd_join(L, L0, U, S),
zdd_join(R, R0, V, S),
cofact(Z, t(A, U, V), S)
; zdd_join(L0, X, U, S),
cofact(Z, t(A0, U, R0), S)
)
).
%
card(X, Y, S):- setup_call_cleanup(
open_state(M),
card_with_memo(X, Y, S, M),
close_state(M)).
%
card_with_memo(I, I, _, _):- I < 2, !.
card_with_memo(I, C, S, M):- memo(I-C, M),
( nonvar(C) -> true
; cofact(I, t(_, L, R), S),
card_with_memo(R, Cr, S, M),
card_with_memo(L, Cl, S, M),
C is Cl + Cr
).
Have a happy new year 2024 !