Toward ZDD library is SWI-Prolog (Useful Code) - Reply 1

General
1

This looks incredible …

Unfortunately, its way to terse for me to understand.

If you could find the time to write a short tutorial – starting from the very simple example … to illustrate use, that would be great.

Dan

2

A tutorial, for example BDDs - Binary Decision Diagrams, if I remember correctly,
is a main conceptual resource of my zdd library. I learned two things there

  1. A zdd represents a family of sets of ordered atoms (urelements).
  2. Minato’s zero suppress rule of ZDD guarantees Axiom of Extensionality of the set theory.

That’s all. I have no idea how to add to the tutorial about ZDD better than possibly many similar
tutorials on the net. Unfortunately I am a person who is good at explain simple things in difficult ways. But I will try to find time to write a simple codes which might be help to explain clearly internal behavior of my zdd library. Anyway, IMHO, above 1 and 2 are essential of ZDD.

3

This is a code which writes given a zdd (family of sets) as a set of
equations. It is almost a flat solved form of A. Colmerauer. Also it
is a special simple case of coalgebra, though it is mainly for non-well founded structure. (ZDD is for well-founded, correct ?)

% ?- open_state(S), zeval(pow([a, b, c, d, e, f]), I, S), show_family(I, X, S),
%	maplist(writeln, X).
%@ 7=t(a,6,6)
%@ 6=t(b,5,5)
%@ 5=t(c,4,4)
%@ 4=t(d,3,3)
%@ 3=t(e,2,2)
%@ 2=t(f,1,1)
%@ []

show_family(I, X, S):- show_family(I, X0, [], S),
	zdd_sort(X0, X1, S),
	reverse(X1, X).
%
show_family(0, X, X, _).
show_family(1, [[]|X], X, _).
show_family(I, X, Y, S):- memo(visited(I)-F, S),
	(	nonvar(F) 	->	Y = X
	;	F = true,
		cofact(I, t(A, L, R), S),
		X = [I=t(A, L, R)|X0],
		show_family(L, X0, X1, S),
		show_family(R, X1, Y, S)
	).

EDIT 2021.11.30

I have added codes zdd_eqns to convert such a system of equations to a family of sets in ZDD:

?- open_state(S), Eqns=[x=t(a,y,z), y=t(b, 0, 1), z=t(c, 0, 1)],
	zdd_eqns(Z, Eqns, S), memo(solve(x)-X, S), zdd_eqns(X, Es, S).
@ S = ..,
@ Eqns = [x=t(a, y, z), y=t(b, 0, 1), z=t(c, 0, 1)],
@ Z = X, X = 4,
@ Es = [4=t(a, 2, 3), 2=t(b, 0, 1), 3=t(c, 0, 1)].

However it does not always correspond to a family of sets in ZDD. For example,
[x=t(b,y,1), y=t(a, 0, 1)] violates the underlying ordering on atoms a < b in this case. In fact, the predicate zdd_eqns/3 was coded as a bidirectional converter between families of sets and systems of equations with above mentioned violation message when found.

This query converts the power set of atoms {a, b, ..., z} to its system of equations, and recovers the original power set from the equations. Details are omitted.

?- time((open_state(S),
	     zeval(pow(@charlist($(a-z))), X, S), 
         zdd_eqns(X, Es, S),
	     zdd_eqns(J, Es, S))).
@ % 12,347 inferences, 0.030 CPU in 0.030 seconds (100% CPU, 407317 Lips)
@ S = ..,
@ X = J, J = 27,
@ Es = [27=t(a, 26, 26), 26=t(b, 25, 25), 25=t(c, 24, 24), 24=t(d, 23, 23), 23=t(e, 22, 22), 22=t(f, 21, 21), 21=t(g, 20, 20), 20=t(..., ..., ...), ... = ...|...].
4

Thank you.

I am curious, how expensive is it to construct families so that efficient set operations on many families can be performed?

5

I have only a partial answer. Sometimes a family of sets is easier to be represented efficiently than the way which uses a list of sets. An extreme example is the powerset of a set, which
use only N nodes where N is the cardinality of the set. If the purpose is to get the cardinality, it is not necessary to count one by one for 2^N elements, but only N iterations of simple arithmetic suffice with appropriate small tabling. A family of sets is a first-class citizen in ZDD.

I believe good answers are on the net for you, which also I would like to know.

6

Thank you.

I think I wasn’t clear enough with my question …

Suppose ZDD is a great representation for a family of sets – but, the ZDD representation must be constructed our of, say, a search algorithm.

I wonder what the cost is to create a ZDD based representation … vs. for example to use conventional methods

7

I rely on term_hash/4 for building families of sets. However, I think its cost is almost negligible compared with complexity for solving the goal of the problem, in which the family of sets tends to grow exponentially large. I am still learning that pruning is essential to solve problems in ZDD.