Thank you for the link, I will check later. As you know, I am a person who didn’t know EXOR nor NAND.
They were mere macros for me until your notice. Thanks for that. So I think, it would be much better for you to find other researchers to talk about the subject. I have to keep silent on that. Sorry.
As for me, I have not a dream at all on my hobby programming, but rather I have a question for a long time why functor/setarg/term_hash programming is not so popular in (SWI-) Prolog. In this sense, ZDD may be a small dream for me to show positively such user programming in Prolog. My dream is much much smaller than yours.
Seems to return the same answers. I feel at ease.
?- sat_count(X* -X, C).
%@ C = 0.
?- sat_count(X*Y,C), sat_count(X+Y,D).
%@ C = 1,
%@ D = 3.
?- sat_count(X+Y+Z,C).
%@ C = 7.
?- sat(-X+Z), sat(X+Y+Z), sat_count(C).
%@ C = 5.
?- sat(-X*Y), sat(X+Y+Z), sat_count(C).
%@ C = 2.
?- sat(-X*Y), sat(X+Y+Z), sat_count(C), sat_count(X+Y+Z, D).
%@ C = 2,
%@ D = 7.
As for the merge, its a kind of distribution law like this
(a + b) * (c +d) = ...
(a*b) + (c*d) = ...
In boolean, we can use the duality law. So, in fact, in my ZDD they are processed
luckily by the same ltr_merge, which is closely related the famous set of choice functions, which you can see the name ltr_choices in the pack pac (this is untouched since long time ago).
sat_count/2 is history independent, but sat_count/1 is not.
% ?- sat((-X)*Y), sat_count(X*Y,C), sat_count(X+Y+Z,D).
%@ C = 1,
%@ D = 7.
?- sat(-X*Y), sat(X+Y+Z), sat_count(C), sat_count(X+Y+Z, D).
%@ C = 2,
%@ D = 7.
Sorry, my interface is too simple, and simple -minded.
I have to check the macro expansion on +[1|Vs], Thanks.
% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C).
%@ Vs = [A, B],
%@ C = 2.5 .
Fixed. Fixed.
% ?- sat(A -> B), Vs = [A,B], sat(+([1|Vs])), sat_count(C).
%@ Vs = [A, B],
%@ C = 3 .
% ?- sat(A -> B), Vs = [A,B], sat_count(+[1|Vs], Count).
%@ Vs = [A, B],
%@ Count = 4 .
I prefer mine, but of course I do not insist.
No. But there are snapshot tools, sets/2, psa/1, dump_state/0 for debugging only on a small ZDD.
?- zdd((X<<pow([a,b]), sets(X, U))).
?- zdd((X<<pow([a,b]), psa(X))).
?- zdd((X<<pow([a,b]), zdd_dump))).
I am not sure they works on your environment. Unfortunately, emacs on my computers are busy (hang?) to get logs to show here. Anyway I should say again, No.
(EDIT)
% ?- zdd((X<<pow([a,b]), sets(X, Y))).
%@ X = 3,
%@ Y = [[], [b], [a], [a, b]].
% ?- zdd((X<<pow([a,b]), psa(X))).
%@
%@ zdd 3:
%@ []
%@ [b]
%@ [a]
%@ [a,b]
%@ X = 3.
% dump_state ==> zdd_dump
% ?- zdd((X<<pow([a,b]), zdd_dump)).
%@ 2 = t(b,1,1)
%@ 3 = t(a,2,2)
%@ X = 3.
It seems difficult because constraints are kept as DNF. To dump the DNF as it is may be only possible like this.
% ?- zdd((dnf(X+Y, U), sets(U, V), get_key(varzip, W), extern(V, A))).
%@ U = 4,
%@ V = [[$2], [$1]],
%@ W = [Y- $2, X- $1],
%@ A = [[Y], [X]] .
% ?- zdd((dnf(X->Y, U), sets(U, V), extern(V, A))).
%@ U = 4,
%@ V = [[$2], [- $1]],
%@ A = [[Y], [-X]] .
I have no other idea.
Yes.
ZDD is a set of sets. DNF is a set of clauses. Operations on two groups are very similar but with critical difference. They share the same core in common. So they coexist. I do not explain more here.
EDIT
I have in mind an observation on polynomials over the boolean ring 0,1,+,. First, note that a DNF is a polynomial over the boolean algebra. For example, [[a,x],[b,y], []] => ax+b*y+1. In this sense, a polynomial over the boolean ring should be possible to be efficiently represented in ZDD. Following this simple obsersavation, I have tested a tiny sample that gf2_join/3 below work as a basic operation
on the polynomials over the boolean ring. Here, gf2_join is the only predicate necessary for this test.
Furthermore as the boolean ring is the Galois field GF(2), this observation has interesting consequence. For example the broader Groebner base calculus might be available for normal basis for given boolean ring polynomials, which is critical for many purpose.
If this observation is something correct, all what I think about boolean ring already must have been realized. Anyway I would like to go further a little bit.
gf2_join(X, Y, Z):- shift0(gf2_join(X, Y, Z)).
% %
gf2_join(X, X, 0, _):-!.
gf2_join(0, X, X, _):-!.
gf2_join(X, 0, X, _):-!.
gf2_join(1, X, Y, S):-!, gf2_join_1(X, Y, S).
gf2_join(X, 1, Y, S):-!, gf2_join_1(X, Y, S).
gf2_join(X, Y, Z, S):-
( X@<Y -> memo(gf2_join(X,Y)-Z, S)
; memo(gf2_join(Y,X)-Z, S)
),
( nonvar(Z) -> true %, write(.)
; cofact(X, t(A, L, R), S),
cofact(Y, t(A0, L0, R0), S),
compare(C, A, A0),
( C = (<) -> gf2_join(L, Y, U, S),
cofact(Z, t(A, U, R), S)
; C = (=) -> gf2_join(R, R0, U, S),
gf2_join(L, L0, V, S),
cofact(Z, t(A, V, U), S)
; gf2_join(L0, X, U, S),
cofact(Z, t(A0, U, R0), S)
)
).
%
gf2_join_1(0, 1, _):-!.
gf2_join_1(1, 0, _):-!.
gf2_join_1(X, Y, S):-!, cofact(X, t(A, L, R), S),
gf2_join_1(L, L0, S),
cofact(Y, t(A, L0, R), S).
% (a + b) + (a + b) = 0.
% ?- zdd((X<< (set([b])+set([a])), galois_field:gf2_join(X, X, Z), psa(Z))).
%@
%@ 0
%@ X = 4,
%@ Z = 0 .
% (a + b + 1) * (a + b + 1) = a*b + a + b +1
% ?- zdd((X<< (1 + set([b])+set([a])), zdd_merge(X, X, Z), psa(Z))).
%@
%@ zdd 7:
%@ []
%@ [b]
%@ [a]
%@ [a,b]
%@ X = 5,
%@ Z = 7 .
X is a DNF for given proposition F.
Yes, if no other clause exists.
ODNF is not assumed, but DNF.
Yes, but it is a ZDD for DNF. Without ZDD, DNF is often more difficult for large propositional formula.
This is my experience.
Sure.
% ?- zdd((dnf((A+B)*(C+D)*(E+F), F), sets(F, G))), maplist(writeln, G).
%@ [$2,$3,$5]
%@ [$2,$3,$6]
%@ [$2,$4,$5]
%@ [$2,$4,$6]
%@ [$1,$3,$5]
%@ [$1,$3,$6]
%@ [$1,$4,$5]
%@ [$1,$4,$6]
This is out of my reach. Sorry.
Seems interesting thought. Personally I like such direction. I wish you get something. Take time and proceed. I am struggling with a kind of Groebner base over GF(2) calculus in ZDD programming. So far I got nothing to post here, but interesting for me as ZDD programming.
For me ZDD library is merely a collection of familiar operations on sets of sets over linearly ordered ground terms of Prolog. Internally it is just a Prolog programming based on functor/setarg/term_hash for efficient computation purpose. That’s all. So I am not in a position to comment on interface with the boolean constraint, which is so well designed. However, through discussions and my programming experience on ZDD, a class of zdd(X) already might have vaguely been appearing, where X is set, Boolean algebra, boolean ring (GF(2)), in which they share generic set theoretical operations.
%@ % 45,028 inferences, 0.004 CPU in 0.004 seconds (98% CPU, 10449756 Lips)
%@ C = 16807.
pac-1.5.7 is still underway. pac-1.5.6 has serious bugs at least on macro expansion. I forgot that old sat_count. I thought sat_count is new, only in the next version. The new one seems work correct.
% ?- sat_count(A + B, C).
%@ C = 3.
I am ashamed that I know nothing about Quine or Vidal form.