Autumn Challenge 2023: Lion and Unicorn

[kuniaki.mukai]

@j4n_bur53

XOR forms

I don’t know “XOR form”, sorry, but only “XOR” may be an operation on GF(2) (Boolean Ring). I will check it later.

[kuniaki.mukai]

Thanks I digest later. Something new for me exists, I hope.

BTW. On counting solutions of polynomial = 1 over GF(2), adding hash shows great improvement, which surprised me. Of course this is a special case, but it shows ZDD might be powerfully useful for problem having many substructures sharing.

% ?- N=1000, findall(a(I), between(1, N, I), A),
%	time((zdd gf2_poly_card(+(A), C))).  % 70 second.
%@ % 49,222,352 inferences, 5.406 CPU in 5.488 seconds (98% CPU, 9105667 Lips)
%@ N = 1000,
%@ A = [a(1), a(2), a(3), a(4), a(5), a(6), a(7), a(8), a(...)|...],
%@ C = 5357543035931336604742125245300009052807024058527668037218751941851755255624680612465991894078479290637973364587765734125935726428461570217992288787349287401967283887412115492710537302531185570938977091076523237491790970633699383779582771973038531457285598238843271083830214915826312193418602834034688.

[kuniaki.mukai]

@j4n_bur53

the Japanese name

for XOR

XOR = exclusive-or, I heard. I didn’t pay attention to XOR, NAND as “non standard” operations name.
‘and, or, not’ are all I am familiar with (like most of others ?).

[j4n_bur53]

@kuniaki.mukai

Anyway, programming on ZDD in SWI-Prolog is a hobby of mine.

Do you think somebody would understand your code, if you would
get run over by a street car tomorrow? Does it have comments?

I have to ask the same myself, I have deleted tree.p, etc… from here.

[kuniaki.mukai]

I added %! comments to almost predicates there, which was exceptionally efforts of mine.
Anyway I will review ‘zdd.pl’ and ‘zdd-array.pl’.
To be honest, I feel no need to add detail comments because of simplicity of ZDD.

How about write zdd on your system ? I believe
it would be a work of couple of days for experts like you.

[kuniaki.mukai]

@j4n_bur53

Do you have predicate in your library(zdd) that generates and
allows to inspects normal form ZDD?

I never heard about such normal form ZDD, though I am lazy
to learn. I thought they keep always normal form in nature.
Anyway I am glad to hear that you seem to start doing something interesting on ZDD.

[kuniaki.mukai]

@j4n_bur53

Well you might not have heard in spoken words, but you can read about it!

Zero-suppressed decision diagram (ZDD)
In contrast, a node in a ZDD is replaced with its negative child if its positive edge points to the terminal node 0. This provides an alternative strong normal form, with improved compression of sparse sets. It is based on a reduction rule devised by Shin-ichi Minato in 1993.

(I must answer in short. ) I think I understand correctly the note
by Minato. If one think in terms of families sets, the Minato’s note
in conjunction with labelled binary DAG representation of a family of sets becomes obvious. (In fact, I posted a related note somewhere sometime). So still I think my implementation is faithful to Minato’s rule.

[j4n_bur53]

@kuniaki.mukai

So still I think my implementation is faithful

Maybe not faithful enough as that it would generate the ZDD
normal form. Possibly a bug or wrong interpretation of the set
notion. The set notion alone doesn’t give you ZDD.

It only shows composition and decomposition along
one Propositional variable into co-factors. Its the ordinary
Boolean Expansion. That is what ZDD and BDD share.

But then you need more to arrive at ZDD.

Boolean Expansions:

f_-Xk = f(X1,...,Xk-1,0,Xlk+1,..,Xn)
f_Xk = f(X1,...,Xk-1,1,Xlk+1,..,Xn)
f(X1,..,Xn) = (-Xk)*f_-Xk + Xk*f_Xk

Set Notion:

f_~vk = { s  | s e f & ~vk e s }
f_vk = { s \ {vk} | s e f & vk e s }
f = f_~vk u { s u {vk} | s e f_vk }

But the above alone is not ZDD. Its only BDD if you make
a DAG out of it, with nodes that have the two co-factors.
Where is the compression?

Edit 11.12.2023
Also negative propositional variable -Xk is not { -Xk }. There could be a
second bug, in the implementation of DNF and your sat/1. If you can
form singletons { -Xk } then you have a kind of 3-valued logic, its

not anymore Boolean expansion. You call zdd_singleton/3
with a negative literal. But since I installed release 9.1.20 of SWI-Prolog
I cannot run library(pac) 1.8.3 anymore because of some QLF version

error problem. And library(pac) 1.8.5 is broken. You see this here:

Failed to process pack
https://www.swi-prolog.org/pack/list?p=pac

Its not anymore listing the source code.

[kuniaki.mukai]

@j4n_bur53

Maybe not faithful enough as that it would generate the ZDD
normal form. Possibly a bug or wrong interpretation of the set
notion. The set notion alone doesn’t give you ZDD.

l could not understand your doubt.
Could you give an input-output example which shows clearly that my implementation has bugs or is not faithful to Minato’s rule. Thanks.

[j4n_bur53]

@kuniaki.mukai

give an input-output example which shows clearly that my implementation has bugs

I already gave Example 1 and Example 2 here:

https://swi-prolog.discourse.group/t/autumn-challenge-2023-lion-and-unicorn/6949/78

https://swi-prolog.discourse.group/t/autumn-challenge-2023-lion-and-unicorn/6949/79

But its an indirect example since I am looking at what sat/1 and psa/0 do.
I already asked you for better inspection predicates, like a predicate
that can show the ZDD tree. But you didn’t respond.

[kuniaki.mukai]

@j4n_bur53

I already asked you for better inspection predicates, like a predicate
that can show the ZDD tree. But you didn’t respond.

Sorry for that. I had checked in fact, but could not find your point which entails bugs of my implementation or my being unfaithful to Minatos’s rule.

[j4n_bur53]

@kuniaki.mukai

Sorry for that. I had checked in fact, but could not find your point
which entails bugs of my implementation or my being unfaithful to Minatos’s rule.

Well if you would compute Minatos ZDD normal form.
Then this here, Example 2:

?- sat((-a)*b+a*b), psa.
 zid = 7
        [-a,b]
        [a,b]

And this here:

?- sat(b), psa.
 zid = 2
        [b]

Would have the same ZDD. But it shows me two different results.

Why? Same problem with Example 1. Possibly to do that you
use 3-valued logic and not 2-valued logic. Your sat/1 predicate
doesn’t do what for example Markus Triskas sat/1 does?

Edit 11.12.2023
One could use Markus Triskas ZDD implementation to verify my claims.
It usage is as follows, before using sat/1, you must call zdd_set_vars/1
with a list of all Boolean variables that occur in your model.

https://github.com/triska/clpb/tree/master/zdd

Markus Triskas ZDD is already 8 years old, not sure whether
it still works. But if I remember well, it can show the resulting
ZDD. So could check against Markus Triskas ZDD.

My library is much simpler, there is no zdd_set_vars/1, its
just a parameter to tree3_eval/3:

@j4n_bur53

Source code of my take on library(zdd), no sharing or memoization, but already
producting ZDD normal form. As a bonus it contains a ZDD XOR operation,
surprisingly can be implemented without knowing the variable list:

tree3.p.log (5,0 KB)

[j4n_bur53]

@j4n_bur53

before using sat/1, you must call zdd_set_vars/1

Here the Example 1 and Example 2 with Markus Triska:

Example 1:

?- zdd_set_vars([A,B]), sat(A=\=B).
node(5)-(A->true;node(3)),
node(3)-(B->true;false),

?- zdd_set_vars([A,B]), sat(~(A=:=B)).
node(6)-(A->true;node(3)),
node(3)-(B->true;false),

Example 2:

?- zdd_set_vars([A,B]), sat((~A)*B+A*B).
node(4)-(A->node(3);node(3)),
node(3)-(B->true;false),

?- zdd_set_vars([A,B]), sat(B).
node(4)-(A->node(3);node(3)),
node(3)-(B->true;false),

Lets see whether what Markus Triska produces as ZDD normal
form, is the same what my tree3.p produces as ZDD normal form:

@j4n_bur53

Example 1 works fine:

?- tree3_eval((a=\=b), [a,b], X).
X = (a->1;b->1;0).

?- tree3_eval(-(a=:=b), [a,b], X).
X = (a->1;b->1;0).

So the tree is a->1;b->1;0, which is the same as, we can start
with node(5) or node(6) doesn’t matter:

node(5)-(A->true;node(3)),
node(3)-(B->true;false),

Just replace node(3) by its definition and you get:

node(5)-(A->true;(B->true;false)),

Same tree as found by my tree3.p. Next example:

@j4n_bur53

Example 2 works fine:

?- tree3_eval((-a)*b+a*b, [a,b], X).
X = (a->(b->1;0);b->1;0).

?- tree3_eval(b, [a,b], X).
X = (a->(b->1;0);b->1;0).

So the tree is (a->(b->1;0);b->1;0), which is the same as

node(4)-(A->node(3);node(3)),
node(3)-(B->true;false),

Just replace node(3) by its definition and you get:

node(4)-(A->(B->true;false);(B->true;false)).

Same tree as found by my tree3.p.

[j4n_bur53]

Can the same validation of a ZDD normal form be done with
your zdd(zdd) from your library(pac) ? Does your zdd(zdd) have
these two functions somewhere:

1. Input Propositional Formula:
   Enter a propositional formula, consisting of - (negation),
   + (disjunction), * (conjunction), etc… and propositional variables a, b, etc…
   Like is possible in my tree3.p or in Markus Triskas ZDD library.

2. Output ZDD Normal Form:
   Request the computation of ZDD normal form and display the resulting
   ZDD normal form, i.e. the tree, either expanded (like in my tree3.p) or
   as a list of nodes (like in Markus Triska)

Does your zdd(zdd) from your library(pac) have 1) and 2) somewhere?
And if yes, can you give an example how to use it?

[kuniaki.mukai]

@j4n_bur53

Would have the same ZDD. But it shows me two different results.

For a given formula P, my sat constructs simply an equivalent DNF Q of P. Q is not always a “normal form” of P. I don’t know what is the normal form in your sense. However my sat can enumerate from Q and the number of variables appearing in P the number of assignments which gives true to the input P.

In addition, my sat is built on ZDD, and ZDD has the normal form in
nature (IMO). In other words, my sat is a merely incremental DNF converter application built on ZDD as a family of sets of literals by giving simply a special ordering on literals (ltr_compare/3). I should have put emphasis on this.

[j4n_bur53]

@kuniaki.mukai

I don’t know what is the normal form in your sense.

Please stop talking nonsense. Its not in “my sense”. There is no such thing
as “my sense”. Its defined in this paper, I was refering to this paper allready
like a 100 times. You are just ignoring what I am refering to and pretend

I would invent something. Whats wrong with you? Where did you learn
accusing people of not knowing what they are talking about? Its extremly
simple the normal form is explained in this paper with like a dozen

examples and pictures showing the normal form. Every tree in the paper
that is supposed to be a ZDD, is a tree in ZDD normal form:

@j4n_bur53

Zero-suppressed BDDs and their applications
Minato, Shin-ichi - 2001
https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf

@kuniaki.mukai

ZDD has the normal form in nature (IMO).

Also my request to document your ZDD library and give guidance is very
simple. Show how to input a propositional formula and output the ZDD
normal form. I don’t care if you call it ZDD normal form in nature, or normal

form in heaven, or normal form in hell. I really don’t care how you call it.
The common understanding should be extremly simple, since I was refering
to the Minato paper. Can you produce the tree thing described in the Minato

paper, and not the set thing? Can you please show the “normal form in
nature” for this propositional formula:

/* Negation of Conjunction */
- (A * B)

And can you please explain how do I use your library to show the “normal form
in nature” of the above propositional formula.

[j4n_bur53]

(Nothing of importance)

[j4n_bur53]

(Nothing of importance)

[kuniaki.mukai]

@j4n_bur53

how can I view the ZDD normal form result?

I wrote a small codes show_fos/2 to show a fos (family of sets).

% ?- zdd zdd_singleton(a, X), show_fos(X).
%@ 2->t(a,0,1)
%@ X = 2.

% ?- zdd X<< {[a,b], [b,c]}, show_fos(X).
%@ 6->t(a,5,2)
%@ 5->t(b,0,4)
%@ 4->t(c,0,1)
%@ 2->t(b,0,1)
%@ X = 6.

% ?- zdd X<< pow([a,b]), show_fos(X).
%@ 3->t(a,2,2)
%@ 2->t(b,1,1)
%@ X = 3.

Property of → : In ZDD -> is maintained to keep the
following property. To explain, suppose

 X -> t(A, Y, Z),
 U -> t(B, V, W).

Then
X = U if and only if A=B, Y=V, and Z=W.

This is the property what I meant by “normal form in nature”,
and of course it is an important well-known property of sets called extesionality.

% Codes to show a family of sets in ZDD.

show_fos(X, S):- X > 1,
	accessible_nodes(X, Ns, S),
	forall(	member(M, Ns),
			( cofact(M, T, S),
			  writeln(M->T))).
accessible_nodes(X, Ns, S):-
	accessible_nodes(X, Ns0, [], S),
	sort(Ns0, Ns1),
	reverse(Ns1, Ns).
%
accessible_nodes(X, A, A, _):- X<2, !.
accessible_nodes(X, [X|A], B, S):-
	cofact(X, t(_, L, R), S),
	accessible_nodes(L, A, A0, S),
	accessible_nodes(R, A0, B, S).

[j4n_bur53]

(Nothing of importance)