Counting nodes of ROZDD for a power set or a map space (an experiment).

[Kuniaki Mukai]

Hi,

Let pow(V) be the set of subsets of a set V, and map(D, R) the set of maps from D into R.

With #(S) being the cardinality of a set S, the following are well-known.

#(pow(V)) = 2 ^ #(V).

#(map(D, R)) = #(R) ^ #(D)

How many nodes are there in the ROZDD for the pow(V) or map(D, R) ?

Writing a few lines of codes below to count all intermediate nodes
in the ROZDD as DAG, I got #(pow(V)) and #(map(D, R)) for small sets V, D, R.

Results are, of course, as advertised, which are nevertheless impressive for me.
I hope also for others.

% ?- N=20, time((numlist(1, N, L), solve([X:=pow(L)]), zdd_count_nodes(X, C))).
%@ % 335,140,552 inferences, 53.093 CPU in 54.102 seconds (98% CPU, 6312313 Lips)
%@ N = C, C = 20,
%@ L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = 3145705.

% ?- D = 10, R= 2, numlist(1, D, Dom), numlist(1, R, Ran),
% maps(Dom, Ran, Maps), solve([X:=Maps]), zdd_count_nodes(X, Count).
%@ D = 10,
%@ R = 2,
%@ Dom = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ Ran = [1, 2],
%@ X = 4082,
%@ Count = 20.

% ?- D = 8, R= 3, numlist(1, D, Dom), numlist(1, R, Ran),
% maps(Dom, Ran, Maps), solve([X:=Maps]), zdd_count_nodes(X, Count).
%@ D = 8,
%@ R = 3,
%@ Dom = [1, 2, 3, 4, 5, 6, 7, 8],
%@ Ran = [1, 2, 3],
%@ X = 19672,
%@ Count = 24.

zdd_count_nodes(X, C):- intermediate_nodes(X, [], S),
length(S, C).
%
intermediate_nodes(I, X, Y):-integer(I), !,
( memberchk(I, X) -> Z = X; Z = [I|X] ),
cofact(I, if(_, L, R)),
intermediate_nodes(L, Z, Z0),
intermediate_nodes(R, Z0, Y).
intermediate_nodes(_, X, X).

Kuniaki Mukai

[j4n bur53]

Thats very nice. I dunno yet how to make the conversion
of map(D, R) to BDD quickly. For pow(V) it was easy.
For pow(V) I used the condition ~W1, .., ~Wn, where W1,..,Wn

were the remaining variables outside of V. But for map(D, R),
I dunno yet how to generate a boolean condition. Your observation
is justified, assuming that map(D, R) is a circuit that often happens,

there is some benefit if a tree can encode this compactly. And you
somehow already showed that ROZDD can do it compactly.

Cool!

[j4n bur53]

How do you encode pairs needed in a function?
Basically map(D,R) is the following set:

    map(D,R) = { F | F subset DxR, F functional }

But you wrote:
%@ Dom = [1, 2, 3, 4, 5, 6, 7, 8],
%@ Ran = [1, 2, 3],

So what is your map(D,R), can you show us?
I don't think map(D,R) can be converted into a
ROZDD, looks rather impossible to me. One

element F of map(D,R) can be converted, but
map(D,R) itself, I don't think so. One F would be
a family of sets if D,R are disjoint and pairs

are {a,b}. But then map(D,R) is a family of
families of sets. So what did you do Kunai?

[j4n bur53]

Can you show the result of maps(Dom, Ran, Maps)?

[j4n bur53]

You see that something is wrong, by the count you are showing.

First you write:

> #(map(D, R)) = #(R) ^ #(D)

But then you get:

> % ?- D = 8, R= 3, numlist(1, D, Dom),  numlist(1, R, Ran),
> %        maps(Dom, Ran, Maps), solve([X:=Maps]), zdd_count_nodes(X, Count).

> %@ Count = 24.

So there are two questions.
- You assume zdd_count_nodes notes is same as cardinality #(_) ?
- What is #(R) and #(D) supposed to be, this is count not of a
  family of sets, but of  a set, right? So you would get:
       #(R) = 3
       #(D) = 8    right?
- Did you check the formula, accordingly to you formula, you
   should now have:
      #(map(D, R)) = #(R) ^ #(D) = 3 ^ 8 = 6561
- But I don't see 6561 somewhere?

[Kuniaki Mukai]

Here is codes for maps/3, which is usual Prolog codes like append/3, 

and the number 6531 (= 3^8 ) seems to appear  in the output of a   query on the maps/3.

% ?- maps([1,2,3,4,5,6,7,8],[1,2,3], Asg), length(Asg, Len).

%@ Asg = [[1-1, 2-1, 3-1, 4-1, 5-1, 6-1, 7-1, ... - ...], [1-1, 2-1, 3-1, 4-1, 5-1, 6-1, ... - ...|...], [1-1, 2-1, 3-1, 4-1, 5-1, ... - ...|...], [1-1, 2-1, 3-1, 4-1, ... - ...|...], [1-1, 2-1, 3-1, ... - ...|...], [1-1, 2-1, ... - ...|...], [1-1, ... - ...|...], [... - ...|...], [...|...]|...],

%@ Len = 6561.

maps([], _, [[]]).

maps([X|Xs], Range, Fs):- maps(Xs, Range, Gs),

maps(Range, X, Gs, Fs, []).

%

maps([], _,  _, Fs, Fs):-!.

maps([Y|Ys], X, Fs, Gs, Hs ):- extend_maps(Fs, X-Y, Gs, Ms),

maps(Ys, X, Fs, Ms, Hs).

%

extend_maps([], _, Hs, Hs).

extend_maps([F|Fs], A, [[A|F]|Hs], Gs):-

extend_maps(Fs, A, Hs, Gs).

Kuniaki Mukai

--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.
Visit this group at https://groups.google.com/group/swi-prolog.
For more options, visit https://groups.google.com/d/optout.

[j4n bur53]

k, map(D, R) can be huge, do you have some structure sharing.
Maybe lets only look at members of map(D, R), individual
functions f : D -> R, they can be really useful.

I find a funny notation in this paper

Simplicity: A New Language for Blockchains

Russell O’Connor roco...@blockstream.com

2017-12-13

https://blockstream.com/simplicity.pdf

He writes for example sha-256-block : 2256 × 2512 ⊢ 2256, which
can be read as a function that sends a bitvec of length 256 and
a bitvec of length 512 to a bitvec of length 256.

He does some counting of the tree size in his language and
he reports:

Our Simplicity expression consists of 3 274 442 combinators. However,

this counts the total number of nodes in the abstract syntax tree that makes

up the expression. Several sub-expressions of this expression are duplicated

and can be shared. Imagine taking the abstract syntax tree and sharing identical

sub-expressions to create a directed acyclic graph (DAG) representing the

same expression. Counting this way, the same expression contains only 1 130

unique typed sub-expressions, which is the number of nodes that would

occur in the DAG representing the expression.

Can you do sha-256-blockwith ROZDD?
How large does it get?

[j4n bur53]

I got an idea how a translation of map(D,R) could be done, also
with Prolog Variables, and possibly with a lot of sharing. I would
require D disjoint from R. But then we could define two new operations:

    1) Operation Pair: R=pair(V,W):
            V variable in, W variable in, R variable out
                    gives a new variable, with the condition R=:=[[V,W]]
                    more or less. It would need the family of sets such,
                    that R itself is not used in the modelling of the family,
                    since its a new variable.

     2) Operation Insert: S=insert(F,R):
              F family of sets in, R variable, S family of sets out
                    gives a new family, if the F=[A1,..,An] then
                   S=[[R|A1],..,[R|An]]. But somehow, like pair it should
                   be a logical operation with a lot of sharing.

You can then build map(D,R) as follows:

     map([],_)=[[]]

     map([C|D],[A1,..,An]) = insert(H,B1)+..+insert(H,Bn)
         where H=map(D,[A1,...,An])
                    B1=pair(C,A1)
                    ...
                    Bn=pair(C,An)

But still non trivial to implement. Especially the pair think. I am
still think maybe can do something simpler. Not yet sure.