I don’t know “XOR form”, sorry, but only “XOR” may be an operation on GF(2) (Boolean Ring). I will check it later.
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.
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 ?).
1 Like
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.
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.
How can I test your ZDD? Your ZDD seems not to work
as in Minatos paper. Minatos paper suggests this reduction:
Zero-suppressed BDDs and their applications
Minato, Shin-ichi - 2001
https://eprints.lib.hokudai.ac.jp/dspace/bitstream/2115/16895/1/IJSTTT3-2.pdf
I am assuming that this leads to a normal form? When
I am playing I don’t see that it generates normal forms,
there are different zid’s for logically equivalent formulas.
Example 1 with different zid’s:
/* Assuming @kuniaki.mukai pac is already installed */
?- use_module(library(pac)), use_module(zdd(zdd)).
true.
?- sat(a=\=b), psa.
zid = 8
[-a,b]
[a,-b]
-------------------
true.
?- sat(-(a=:=b)), psa.
zid = 10
[-a,b]
[a,-b]
-------------------
true.
Example 2 with different zid’s:
?- sat((-a)*b+a*b), psa.
zid = 7
[-a,b]
[a,b]
-------------------
true.
?- sat(b), psa.
zid = 2
[b]
-------------------
true.
Do you have predicate in your library(zdd) that generates and
allows to inspects normal form ZDD?
On my side, I have already such a library(zdd), thanks to my daily Prolog
procrastination. For a given variable ordering it generates identical normal
forms, for logically equivalent formulas.
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).
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).
Edit 10.12.2023
But the example 2 shows that I have a different approach than
yours concerning propositional variables. I don’t see doing the
same in your zdd_singleton/3 predicate from your library(zdd).
I am sticking to Minatos paper, where he shows how to model, for example
the negated propositional variable ~d as {***0} where * indicates don’t care.
Similary you would model the positive propositional variable d as {***1}
by introducing a further node, not shown here:
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)
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.
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.
https://en.wikipedia.org/wiki/Zero-suppressed_decision_diagram
I didn’t hear it in spoken words either, only saw it here in this diagram:
You sure your library(pac) works correctly? Why are there different zids?
Is this specific to your sat/1 predicate, that it allows different zids, or
is there some other reason. Because it can generate unique zids sometimes:
?- sat(a+c+b), psa.
zid = 7
[c]
[b]
[a]
-------------------
true.
?- sat(c+a+b), psa.
zid = 7
[c]
[b]
[a]
-------------------
true.
?- sat(a+b+c), psa.
zid = 7
[c]
[b]
[a]
-------------------
true.
But it should generate always unique zids. So maybe there is a bug
somewhere in your library? Or its even not ZDD that you implemented,
but something else. Only the predicates have zdd_XXX names,
but its not really ZDD what your library provides. At least not a ZDD
as Shin-ichi Minato describes it in figure 4?
(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.
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.
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.
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.
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:
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:
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:
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.
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:
-
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. -
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?
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.
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:
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.
Its not clear what you mean by “emphasis”. You still keep
talking that you have somewhere ZDD. You write stuff like
“my sat is built on ZDD”. But how can I access your ZDD?
Is this possible? Can I do the following, yes or no?
By ZDD normal form, we mean the tree thing described here. Trees where
the author Minato says they are ZDD. Not where myself or Markus Triska say
they are ZDD, but where Minato says they are ZDD: