Autumn Challenge 2023: Lion and Unicorn

Example
96 

% ?- zdd dnf(-(a*b), X), show_fos(X).
%@ 4->t(-a,3,1)
%@ 3->t(-b,0,1)
%@ X = 4.
97

Thats not a ZDD normal form. A ZDD normal form is akin to a unate cube,
only using positive literals. Also your form is not reduced, ZEROS ARE NOT
SUPRESSED, you have t(-b, 0, 1), a zero appears in the left co-factor.

But I am not sure whether your binate form can even suppress the same way
that an unabte form can suppress? But if we would allow x to be either v
or ~v, the reduction t(-b, 0, 1) would replaced it by 1:


https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf

So maybe reduction is missing. And its not unate. What you did is using
someting akin to a binate cube. But t(-X,A,B) is the same as t(X,B,A).
So its not really needed, unless you want to represent something

else than ZDD normal form. And that is what you do, you represent
something else than ZDD normal form. You didn’t implement unate
ZDD, or you implemented somewhere unate ZDD, but you didn’t use

unate ZDD in the “eval” part of “eval_and_show_XXX”.

Edit 12.12.2023
Here you see the result in Markus Triska. Its the same what my tree3.p
generates. No negative propositional variable needed, and its reduced, i.e.
no false appears in the left co-factor, ZEROS ARE SUPRESSED:

/* Markus Triskas ZDD normal form */
?- zdd_set_vars([A,B]), sat(~(A*B)).
node(6)-(A->true;node(0)),
node(0)-(B->true;true)
98

(Nothing of importance)

99

IMO, essence of zero-suppress rule is to keep the extensionality of
families of sets represented in binary DAG, for not including redundant nodes. So far, I could not find other meaning of the rule.
I am looking forward to have chance to talk to a really expert on zdd about this.

100

Yes. However ltr_card/3 counts somehow correctly 3.

% ?- zdd dnf(-(a*b), X), show_fos(X), ltr_card(X, C).
%@ 4->t(-a,3,1)
%@ 3->t(-b,0,1)
%@ X = 4,
%@ C = 3.
101

(Nothing of importance)

102

The triple t(X, A, B) means the union of

  • the family A, and
  • the family { C | C is the union of the singleton {X} and set D in
    the family B}.

So, if B is the empty family then t(X, A, B) means A; t(X, A, 0) = A.
This is my interpretation of the zero suppress rule. Is this meaningless ?

103

(Nothing of importance)

105

l have downloaded the pdf, which seems be protected. So I could not search “ZDD normal form”. Could you tell the place in the pdf
if “ZDD normal form” is really defined.

BTW, in the ltr_card/3 below, given DNF is expanded
so that the number of clauses which leads to 1 is the sat count, though I forgot details.

ltr_card(In, Out, S):-
	zdd_boole_atoms(Us, S),
	zdd_sort(Us, Vs, S),
	expand_dnf(Vs, In, Y, S),
	card(Y, Out, S).

EDIT
I have skimmed through the pdf. It seems on something like boolean functions, which is irrelevant to what I am doing in pack(ZDD) as library for handling family of sets. Furthermore, if you look into my zdd.pl, you see it also handles families of lists (see all_perm, all_epi, all_mono, all_fun), which I posted recently one yearn ago ?

BTW, I have tested to change the internal triple t(A, L, R) to u(A, R) when L=0. (zero suppressing ! (joking)) by inserting only few lines on the core predicate cofact/3 of my ZDD. As far as I have seen, nothing has happened on overall performance. However, for the time being I use for fun this hybrid DAG representation where binary/unary branches coexist.

108

Sorry if it confuses. It is a joking. I didn’t mean it is zero suppressing at all. When I wrote codes a year ago the all_perm to enumerate all permutions for given a list of n elements, I felt the uniform use of binary dags redundant, and appropriate hybrid use of binary and unary nodes looks more suitable for space efficiency. So now I wanted to replace t(X, 0, R) with u(X, R) just for fun, without changing
semantics as families of sets.

I remember that I started with “if-then-else” semantics in mind after Markus, but I found that I gradually forgot such interpretation.
I had reasons but I can’t explain well for now, but at least because I could not catch up with such smart work, which seemed to me
almost completed work on boolean constraint on Prolog by Markus.

110

No. The number of nodes for the hybrid version is the exactly the same as the uniform one provided that 0 is not counted as a node.

112

No. It is out of my interest, though it is good that you seem
getting professional results on compression (“圧縮”).

115

good to know jan, nice that you always keep me updated… :+1:

123

Happy to hear that