On using ZDD as keys of dict

I am experimenting with idea on using ZDD as keys of dict, in other words, on ZDD which has a value cell for each node. Reflecting on my limited experience on ZDD, ZDD looks like just a kind of dict which uses heavily hashing on keys of the dict. Although I have a goal in mind for this experiment, I am not sure there would be some interesting result for Prolog programming. But I have a small hope for the time being. As ZDD is roughly a kind of boolean algebra, if values in the cell form a similar algebra (i.e. homomorphic), it might contribute to algorithm like path counting in graphs.

If related or similar works are known, I will appreciate if they are shared here.

As my first try, I built powerset zdd (zdd_dict_power/3 below) which stores cardinality in the attached cells. In the code below, zdd_dict is a core predicate, but which is almost my cofact/2 on ZDD without value cells.
Fortunately it works I expected.

:- module(zds, []).

:- use_module(zdd('zdd-array')).
:- use_module(zdd(zdd)).
:- use_module(pac(op)).

% ?- open_zdd_dict, zdd_dict(I, t(a, 0, 1), Val).
% ?- open_zdd_dict, zdd_dict(I, t(a, 0, 1), Val), Val=a.
% ?- open_zdd_dict, zdd_dict(I, t(a, 0, 1), Val), Val=a, zdd_dict(I, X, R).
% ?- open_zdd_dict, zdd_dict(I, t(a, 0, 1), Val), Val=a,
%	zdd_dict(J, t(b, I, I), Val2), zdd_dict(I, _, Val2).
% ?- open_zdd_dict, zdd_dict(I, t(a, 0, 1), Val), Val=a,
%	zdd_dict(J, t(b, I, I), Val2), Val2=c,
%	zdd_dict(J, X, Val3),
%	zdd_dict(K, X, Val4).

% ?- open_zdd_dict.

% ?- b_getval(zdd_dict, R), write(R).
% ?- open_hash(4, R), write(R).

% ?- trace.
% ?- open_zdd_dict, b_getval(zdd_dict, R), write(R).

% ?- open_zdd_dict, zdd_dict_power([a,b], P, C).
% ?- zdd_dict_power([], P, C).
% ?- open_zdd_dict, zdd_dict_power([a,b,c], P, C).
% ?- numlist(1, 100, Ns),open_zdd_dict, zdd_dict_power(Ns, P, C).
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ P = 101,
%@ C = 1267650600228229401496703205376.

zdd_dict_power([], 1, 1).
zdd_dict_power([A|As], X, C):-
	zdd_dict_power(As, Y, C0),
	zdd_dict(X, t(A, Y, Y), C),
	C is C0 + C0.

What about zero-less (L) binary decision diagrams (BDD). So its not
zero-supressed as in ZDD, but zero less as in LDD:

/* BDD you see zeros */
?- tree_eval(a=:=b, X).
X = (a->(b->1;0);b->0;1).

/* LDD you don't see zeros */
?- tree5_eval(a=:=b, X).
X = (a->(b->1;- 1);- (b->1;- 1)).

Maybe it has also some compression benefit. For example the LDD
could share (b->1; - 1) in the above example.

What I also see as a benefit, is that the boolean function is not encoded
in the leaves, but rather in the nodes.

Are there more such encodings?

Also I have a zero-less version, mainly from curiosity and some need to have lists (not in Prolog’s lists) living with ZDD data. This is a copy and paste of a query log.

% ?- N = 100, numlist(1, N, Ns), X=..[f|Ns],
% term(I, X), term(I, Y), X = Y.
%@ N = 100,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = Y, Y = f(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, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100),
%@ I = 102.

Once I posted building all permutations of a given set, which enumerated for larger sets than that the standard prolog exercise could. Since all permutations are equal to each other as set, I noticed that "zero-less BDD "’ is useful.

You cannot see Zero-Less in Family of Sets. They are the same
for any underlying binary decision diagram representation. You have
to look the binary decision diagram itself:

The left tree shows a Binary Decision Diagram that stores
the propositional logic in its leafs. On the other hand the right tree
shows a Zero-Less Decision Diagram which allows the

negation of nodes. It can get away with zero leafs and stores
the propositional logic in its nodes. Even if you would convert the
left into a ZDD it would still have some zeros, because

the ZDD jump would not suppress all zeros.

Perhaps I am missing computaional significance of zero-suppressing of ZDD theory.
More worse I feel I only understand elementary set theoretical
interpretation of ZDD. So I am afraid I also must be missing points of
your zero-less BDD.

By the way, a ZDD as a set of a labeled binary DAGs, has two properties.

  1. two graph A and B in ZDD are isomorhic if and only if
    so are their children in order.

  2. if B is a proper subgraph of of A, then the root node label of B is greater than that of A.

I meant saying by zero-less BDD a family of graphs with condition 1
but condition 2 dropped and even multiple occurrence are allowed,
with lists data structure in mind as a sample of zero-less BDD in
my (wrong) understanding. In fact, I have been polshing
a small library which supports my “zero-less BDD”, in trial/error way slowly.