Toward ZDD library in SWI-Prolog

I have made a quick test for commutative version restricting to symmetric binary operations. I’m happy to see that idea works. I will try also on ZDD version, which I see no problem for. Your FOL version sounds great for generality, but I enjoy somewhat ad hoc manual versions of mine.

% ?-  symm_count_associative_algebra(1, X).
%@ X = 1.

% ?- symm_count_associative_algebra(2, X).
%@ X = 6.

% ?- time(symm_count_associative_algebra(3, X)).
%@ % 4,121,799 inferences, 1.091 CPU in 1.095 seconds (100% CPU, 3776935 Lips)
%@ X = 63.

% ?- call_with_time_limit(180, time(symm_count_associative_algebra(4, X))).
%@ % 1,290,894,487 inferences, 161.322 CPU in 180.000 seconds (90% CPU, 8001973 Lips)
%@ ERROR: Unhandled exception: Time limit exceeded
``
K.M.

Thank you for letting me to see wider context of your work of the model finder. Of course it is interesting for me, but I’m afraid that I have not time to investigate. Anyway many thanks.

K.M.

Yes, interface between unify-hook and my ZDD must be still alive, though I have not touched the interface for a long time (around a couple of years). The idea was that unification of boolean (Prolog) variables as a quotient operation on ZDD. My ZDD had already a simple class of quotient operations, though quotient operations are often expensive.

I learned from Markus to think about sets of truth tables, which drove me little by little to the current ZDD of mine for some reasons.

There remains the counting path problem as final wall to clear. So far, paths of 7 x 7 is the max for me. Minato group records for 21 x 21 based on Knuth’s idea, which seems a miracle for me. However I set 8 x 8 as my next goal.

As for the urls you pointed on counting associative (commutative) algebra, I visited and saw around.
It is strange for me to see that they seems discussing still on the case 5-set or so. I had thought that there are some known generating function on this problem, in other words, smart mathematician already solved this counting problems as a mathematical formula on n of n-set, and I expected to see the formula at some linked sites, but I failed to find it. I am confused.

K.M.

Counting

Slightly editing codes which counts associative algebras with ZDD to count commutative and associative algebras, I ran the codes. The ZDD version shows result for 4-set in a few second, for which non ZDD version of mine got timeout as reported.

% ?-zdd(( count_algebra_with_zdd(1, C))).
%@ C = 1.
% ?-zdd(( count_algebra_with_zdd(2, C))).
%@ C = 6.
% ?-zdd(( count_algebra_with_zdd(3, C))).
%@ C = 63.
% ?-time(zdd(( count_algebra_with_zdd(4, C)))).
%@ % 13,884,312 inferences, 3.683 CPU in 3.683 seconds (100% CPU, 3770064 Lips)
%@ C = 1140.

I would like to take this as showing power of ZDD because even naive, brute-force, and simple-minded use of ZDD get this result. I have to thank you for leading me to get this. In fact, I was reluctant to try this, who wanted to go to other problems in a hurry.

K.M.

Thanks for clarification. I will be carefu on this. BTW, as I posted earlier, the ZDD of mine has already basic tools handling families of clauses of literals based on fundamental operations on ZDD. Furthermore I think such ZDD can be viewed as a state of processing SAT problem in nature. In fact, I see no problem to introduce incremental update of these states because all necessary tools are already done, I think. I will check this in the future. Thank you for showing fresh points for me which I am almost forgetting.

K.M.

I have checked this for n = 100, writing a small codes:

% ?- N = 100, numlist(1, N, Ns), cartesian(Ns, Ns, P),
%	zip(Ns, Ns, Z),  maplist(pred([A-B, (A, B)]), Z, Z0),
%	zdd((X<<pow(P), zdd_super_power(Z0, X, Q),
%		 card(Q, C))), C=:= 2^(N^2-N).
%@ % 38,618,674 inferences, 3.571 CPU in 3.768 seconds (95% CPU, 10814666 Lips)

zdd_super_power(X, Y, Z):- shift(zdd_super_power(X, Y, Z)).
%
zdd_super_power([], P, P, _).
zdd_super_power([A|As], P, Q, S):-
	zdd_super_power(As, P, Q0, S),
	zdd_insert(A, Q0, Q, S).

Amazingly fast ! So, this time, I ran my ltr_card which counts the number of solutions of DNF given.

% ?- time((N=100,  M is N^2,  numlist(1, N, Ns), zdd((X<< Ns, ltr_card(M, X, C))), C=:= 2^(N^2-N))).
%@ % 7,643 inferences, 0.001 CPU in 0.001 seconds (88% CPU, 8897555 Lips)

I hope so, though I’m not sure. Your test/1 reminded me of my ltr_card/3.

| j4n_bur53
October 25 |

  • | - |

This one is also fun, counting the symmetric relations:

axiom('symmetric',
     all(X,all(Y,r(X,Y)-:r(Y,X)))).

My guess is, if the domain size is n, then there are 2^((n^2+n)/2) symmetric relations?


Sounds like a typical mathematical induction. Isn’t it? KM

X<<E is not interesting, I think. It is just for shorthand to write test queries on ZDD. I introduced zdd/1,2,3 to hide shift/reset calls from queries. At this momemt, zdd/1, 2, 3 are flexible like the next query, in whch
shift/reset are hided. Also the second example might be interesting in that the ZDD of mine keeps my old interface with boolean constraint, though I forgot details.

% ?- zdd(zdd(zdd(zdd((X<<pow([a,b]), card(X, C)))))).
%@ X = 3,
%@ C = 4.

% ?- zdd((dnf(A=B, X), dnf(B=C, Y), ltr_merge(X, Y, Z), ltr_card(3, Z, Count))).
%@ X = 10,
%@ Y = 17,
%@ Z = 25,
%@ Count = 2,
%@ put_attr(A, zdd, 2),
%@ put_attr(B, zdd, 3),
%@ put_attr(C, zdd, 4) .

BTW, I have found my ZDD might have Pure Literal Rule for SAT in nature, which can be used to assign truth values to boolean prolog variables early on the way of solving constraints, though I am not interested in interface with SAT problem for now.

K.M.

No. Currently only +,-,*, etc can be nested.

% ?- zdd((X<<(pow([a,b])-pow([a])), card(X, C))).
%@ X = 6,
%@ C = 2.

It should be not a difficult task to extend this kind of syntax sugar, but I met some difficulty for me,
though I spent little time to fix it. I would like to check it later.

KM

It is not mature to discus about syntax of my ZDD, and I am not familiar with ISO thing.

BTW, I have got the following on your example, where exp is an indicator for functional expressions.

% ?- zdd(C<<exp(card(pow([a,b])))).
%@ C = 4.
zdd_eval(Other, A, S)	:- zdd(call(Other, B), S), 	zdd_eval(B, A, S).

% (Was)
% zdd_eval(Other, A, S)	:- call(Other, B),  zdd_eval(B, A, S).

This example is ad hoc, but I hope this is a good symptom for a general functional expressions. card/2 uses shift/1 to get the state inside, which is a reason, I think, why old zdd_eval did not work for the example. Anyway this is ad hoc. I have to be silent about syntax for the time being. Anyway shift/reset
programming is interesting, I feel, to be investigated further.

K.M.

P.S.

With a minimal change of zdd/3, I have found a way to drop the exp indicator above like this.

% ?- zdd((C << card(pow([a,b,c,1,2,3])))).
%@ C = 64.
% ?- zdd((C << card(pow(prolog(append([a,b,c], [1,2,3])))))).
%@ C = 64.

However, instead of dropping exp, I introduced prolog indicator as in the second query in the example.
This way seems clearer, and, moreover, complete. The role of the prolog indicator should be obvious. I will have time to write more details about this upon request.

Yes, perhaps. zdd/1 does not use b_setval, b_getval, assert internally, though setarg, instead, is used heavily for managing hash tables. I will consider to move to your shorter and elegant syntax in the future. At least for the time being, I keep using shift/reset. For my purpose, shift/reset is more flexible than those above. It is often that multiple states are needed for memory efficiency, and so open, export, close operations are necessary. shift/reset seems more flexible for such management. For example, card/ltr_card open temporal states internally and close it on exit to give chances to gc.

K.M.

% ?- zdd((
%	dnf(x, F),	ltr_card(3, F, C), 
%	dnf(-x, G), ltr_card(3, G, D), 
%	dnf(-x + x, H), ltr_card(3, H, E))),
%   C + D =:= 2^3,
%	E   =:= 2^3.
%@ F = 2,
%@ C = D, D = H, H = 4,
%@ G = 3,
%@ E = 8.

It seems that I am confused about your question. My answer is correct in my sense. I should have noticed that one never asks such simple thing.
I need time.

p.s.
I did only what I could. I hope this is related to your question.
Below x=y is a syntax suger for boolean equivalence as usual.

x = y \Longleftrightarrow (x\to y)\land (y\to x)
% ?- zdd((dnf(z = x+y, F), ltr_card(3, F, C))).
%@ C = 4.

% ?- zdd((dnf(z = x+y, F), ltr_card(4, F, C))).
%@ C = 8.

% ?- zdd((dnf(z = z*x+y, F), ltr_card(4, F, C))).
%@ C = 10.
% ?- zdd((dnf(-(x+y+z), F), ltr_card(3, F, C))).
%@ C = 1.
% ?- zdd((dnf(x+y+z, F), ltr_card(3, F, C))).
%@ C = 7.

Perhaps I am missing the point. What is the meaning the symbol “=:=” ? It sounds like a meta symbol something for definitional equation. If so, it is outside the current ZDD of at least of mine.

No. I tried such common subexpression approach two or more years ago, but all my tries did not work well at all. I was not smart enough to get success. So I decided to work this time inside ZDD structures, which is more than I had expected.

Still I must say No, though I may not understand correctly your question. However, after your question, I have checked that the query below works. Of course, the result is correct in my sense, but I am far from sure it is related to your question. memo is a limited version of the table/1 based on term_hash, which is critical for my ZDD system. Sorry for poor documentation.

% ?- zdd(( memo(exp(1)-f((X+Y),2)),  
%        memo(exp(2)-f((-P),1)), 
%		 memo(exp(1)-f(EXP1, N1)),  dnf(EXP1, Z1), ltr_card(N1, Z1, C1),
%		 memo(exp(2)-f(Exp2, N2)),   dnf(Exp2, Z2),  ltr_card(N2, Z2, C2))),
%	C is C1+C2.
%@ EXP1 = X+Y,
%@ N1 = 2,
%@ Z1 = C, C = 4,
%@ C1 = 3,
%@ Exp2 = -P,
%@ N2 = C2, C2 = 1,
%@ Z2 = 6,
%@ put_attr(X, zdd, 2),
%@ put_attr(Y, zdd, 3),
%@ put_attr(P, zdd, 4) .

A simple minded try is this:

% ?- zdd((memo(jb - g(X+Y*Z, 3)), memo(jb - g(E, N)), 
%		dnf(E, D),  ltr_card(N, D, C1), 
%		dnf(-E, F), ltr_card(N, F, C2))), 
%		C is C1 + C2.	
%@ E = X+Y*Z,
%@ N = C2, C2 = 3,
%@ D = 6,
%@ C1 = 5,
%@ F = 13,
%@ C = 8,
%@ put_attr(X, zdd, 2),
%@ put_attr(Y, zdd, 3),
%@ put_attr(Z, zdd, 4) .

p.s.
BTW, I got an amazing time statistics again on the Jan Burse problem, say jburse(n, C) for short here. As the log below, it has done in 20 seconds forall 1\leq n \leq 100 (new !), displaying big numbers. I remember that even jburse(8, C) took time more than one day long a couple of years ago. Moreover, as I posted earlier, watching the output series, I made a conjecture C = 2^{f(n)}, where f(1)=1, f(n)=f(n-1) + n. Jan Burse is silent on this, and I know little about the jburse problem enough to try to find a proof for the conjecture. If either he knows this property or has a proof, I would be very glad because clearly it supports good efficiency and correctness of the simple minded ZDD implementaion of mine. Also it supports a steady step of mine toward ZDD library on SWI-Prolog. I have reasons why ZDD works faster on jburse(n,C), but it may not be time yet to open, because I am not 100 percent sure on correctness of ZDD of mine, and I know, I am a very erroneous human kind.

% ?- call_with_time_limit(100, time(forall(between(1, 100, N),
%			( jburse(N, C),
%			  writeln(jburse(N, C))
%			)))).
%@ % 55,874,903 inferences, 19.153 CPU in 19.256 seconds (99% CPU, 2917236 Lips)
%@ true.

I got this for n = 4, 5, 6.

jburse(4, 64)
jburse(5, 1024)
jburse(6, 32768)

From experiments for other n, I got the conjecture that jburse problem for n has 2^{g(n)-1} solutions as posted, where g(n) is computed by this:

g(0, 1):-!.
g(N, X):-
	N0 is N-1,
	g(N0, X0),
	X is X0 + N.

As for the difference I do not insist, but I would like to know from curiosity a mathematical definition of the problem. Is it well-known one, or your original ? To be honest, the time statistics for n\leq 100 looks unbelievable also for me.

% ?- forall(between(4, 6, N),
%			(	jburse(N, C),
%				N0 is N-1,
%				g(N0, F),
%				C =:= 2^(F-1),
%				writeln(jburse(N, C))
%			)).
%@ jburse(4,64)
%@ jburse(5,1024)
%@ jburse(6,32768)
%@ true.