Revising my old codes on ZDD

General
1

I am checking my codes on ZDD (pack library(pac)/misc/zdd.pl). Now most part of
codes are junk. However some of basic codes are still live powerful enough to
see ZDD merit, which is hard to see in the standard list operations in prolog.
The following two queries show such power, I hope.

?- numlist(1,10000, Ns),  numlist(10, 10000, Ms),
	time(zdd(( F=pow(Ns), G=pow(Ms), S=(F-G), card(S, C)))).
 1,104,164 inferences, 0.084 CPU in 0.099 seconds (85% CPU, 13151229 Lips)

?- numlist(1, 16, R), time(zdd((X=pow(R), Y=pow(R), Z=X**Y, card(Z, C)))).
  132,399,262 inferences, 9.834 CPU in 9.892 seconds (99% CPU, 13463357 Lips)
  C = 1048561 .

Some basic operations used in this queries.

X + Y : union of X and Y.
X * Y : intersection of X and Y.
X - Y : subtraction of X from Y.
merge(X, Y): merge of X and Y.
merge(X, Y) = {C | C is the union of A and B for some A in X and B in Y}
X ** Y : product of X and Y.
X**Y = { P | P is the cartension product B and C for some B in X and C in Y}
pow(A) : power set of A: The set of subsets of A.

I have no information on recent status on ZDD, but I have resumed enjoying zdd
programming. (Prolog progrmming is still one of my hobby.) More than one year ago, a
young friend of mine on computer science gave me a warning on how powerful
Minato’s ZDD program is, showing me a demo site on ZDD with his iPad, which
overwhelmed me enough at that moment. But still I keep my interest in ZDD
programming, because, IMHO, zero-suppress rule of ZDD is a natural
implementation of the axiom of extentionality of the set theory. This simple
view has been very useful for me to write and check correctness of my codes on ZDD.

Kuniaki Mukai

2

Hi Kuniaki,

Thank you for posting on ZDD and reminding me of the library.

How memory and compute intense is its use, compared, for example, to the ord-set – although, i understand that ZDD has much more powerful operators.

thanks,

Dan

3

How can I compare memory and intense ? time/2, profile/1 are
only tools what I remember for that. Statistics is out of my current interest.

In stead, I am trying to apply some of ZDD idea to path counting problem on directed graphs.

I hope to get some meaning result soon for SWI-Prolog people on performance.

Kuniaki Mukai

4

I have finished reviewing old codes of mine on basic zdd operations; union,
intersection, subtraction, merge, insert, remove, and among many others. ZDD
programming, uses the builtin term_hash heavily in the background; in my view,
my zdd programming is storm of hashing. Also current implemetation uses the
builtin shift/reset as basic control.

I have an idea to which I would like to apply among many others, for example,
matricies of paths in graph theory. One year ago, I counted paths in graph
rect(W, H) for W, H =< 7, if I remember correctly, with such matricies, where
rect(W, H) is the familiar grid graph with (W+1)*(H+1) nodes. I hope to extend
this time for rect(10, 10) with more clear concept on ZDD. BTW, “Minato” seems
calculate at least for rect(19, 19) easily, I saw a demo video on the net. I am
far from to know his algorithm.

My zdd library could be used as table/1, though restricted and not elegant. The
following is an example of nested use of ZDD structure, which generates the power
set of a set with cardinality 16, and then calculate the Fibonacci number for
the cardinality of the power set. I hope time statistics is not so bad.
Use_memo is a favorite byproduct of the ZDD library, which is handy
for daily common programming.

% ?- N = 2, zdd((numlist(1, N, L), P<<pow(L), card(P, C), use_memo(fibonacci(C, V)))).
%@ N = P, P = 2,
%@ L = [1, 2],
%@ C = 4,
%@ V = 3 .

% ?- time((N = 16, zdd((numlist(1, N, L), P<<pow(L), card(P, C), use_memo(fibonacci(C, V)))))).
%@ % 4,325,423 inferences, 0.489 CPU in 0.558 seconds (88% CPU, 8853340 Lips)
%@ N = P, P = 16,
%@ L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ C = 65536,
%@ V = 73199214460290552.... (Too many digits).

<pre>
fibonacci(0, 0):- !, memo(fibo(0)-0).
fibonacci(1, 1):- !, memo(fibo(1)-1),
	fibonacci(0, _).
fibonacci(N, F):- memo(fibo(N)-F),
	(	nonvar(F) -> true
	; 	N0 is N - 1,
		N1 is N0 - 1,
		fibonacci(N0, F0),
		fibonacci(N1, F1),
	  	F is F1 + F0
	).

I am interested in “generating function” of graphs. I have a litte knowledge on
generation functions in general but little on specific one on graph. I will
appreciate any pointer on the topics, which so far I failed to search on the
net.

Kuniaki Mukai

5

I have played around with matrix over paths in a graph. I use vectors (functor,
arg, setarg, nb_setarg), and forall/2. I am not familiar with these builtins,
but I feel comfortable. Although I noticed that forall/2 unbinds vriables, when
I met unexpected results. So then nb_setarg ! Fortunately, I have no other problems
so far. nb_setarg/3 looks efficient.

The sample below is: create new matrix with 1000 x 1000 dimension with
initialial elements, and then transpose it. Time statistics looks not so bad.
Codes of new_marix/2 and m_transopse are also below.

?- time(( Dim = 1000-1000, new_matrix(Dim, M),
		forall((between(1, W, I), between(1, H, J)),
				m_nb_setarg(I, J, M, p(I, J))),
		m_transpose(M, Tr_of_M))).
 % 9,015,017 inferences, 0.555 CPU in 0.578 seconds (96% CPU, 16249305 Lips)
 Dim = 1000-1000,
 M = #(..),
 Tr_of_M = #(..).

?- new_matrix(2-3, M), writeln(M).
 #(#(_64304874,_64304880,_64304886),#(_64304906,_64304912,_64304918))
 M = #(..).
%
new_matrix(W-H, Matrix):- length(M0, W),
	maplist(pred(H, ([C]:- length(R, H), C=..[#|R])), M0),
	Matrix=..[#|M0].

%
m_transpose(X, Y):- atom(X), !, Y = X.
m_transpose(X, Y):- dim(X, W-H),  % W>0.
	new_matrix(H-W, Y),
	forall( between(1, H, I),
			(	arg(I, Y, V),
				forall( between(1, W, J),
					   (	m_arg(J, I, X, Aji),
							nb_setarg(J, V, Aji)
					   ))
			)
		  ).

I will appreciate if expert on matirix handling in Prolog suggests anything or
his experience. My current interest is to handle matrix over family of zdd of
path sets in a graph. I am not sure it will work, nevertheless there are several
things I would like to try before I would be too much tired for unknown possible
difficulty which I have not seen yet.

Kuniaki Mukai

6

I have compared time statistics between two versions on transposingmatrix: m_transpose/2 and ya_transpose. ya_transpose/2 looks likemore recommended style. The result says m_transpose is better. I had guessed the opposite. The result might push me to use more freely combination of forall/2, between/3, and nb_setarg/3.

?-  Dim= 1000-1000,
	time((new_matrix(Dim, M), Dim = W-H,
	forall((between(1, W, I), between(1, H, J)),
			(m_nb_setarg(I, J, M, p(I, J)))),
	m_transpose(M, TrM))).
 % 9,015,017 inferences, 0.703 CPU in 0.754 seconds (93% CPU, 12831559 Lips)
 Dim = 1000-1000,
 M = #(..),
 W = H, H = 1000,
 TrM = #(..).


ya_transpose(X, Y):- atom(X), !, Y = X.
ya_transpose(X, Y):- dim(X, W-H),  % W>0.
	new_matrix(H-W, Y),
	ya_transpose(W, H, X, Y, W-H).

%
ya_transpose(1, 1, _, _, _):-!.
ya_transpose(I, 1, X, Y, W-H):-!, I0 is I-1,
	ya_transpose(I0, H, X, Y, W-H).
ya_transpose(I, J, X, Y, Dim):-
	m_arg(I, J, X, A),
	m_arg(J, I, Y, A),
	J0 is J - 1,
	ya_transpose(I, J0, X, Y, Dim).

?- Dim= 1000-1000,
	time((new_matrix(Dim, M), Dim = W-H,
	forall((between(1, W, I), between(1, H, J)),
			(m_nb_setarg(I, J, M, p(I, J)))),
	ya_transpose(M, TrM))).
 % 11,007,017 inferences, 1.086 CPU in 1.116 seconds (97% CPU, 10133751 Lips)
 Dim = 1000-1000,
 M = #(..),
 W = H, H = 1000,
 TrM = #(..).
8

Thanks for input. I will check the link later. I am busy for
writing several my own versions of codes for Minota demo (path count for rectangular n x n,

So far all codes does not work well in efficiency. It remains only one codes left, which looks like

a constructing regular expression on given diagram for regular expressions.

I think such codes are common, e.g. SWI-Prolog ruturns in such a form

for cyclic terms.

Kuniaki Mukai

9

Finally I have managed to polish my prolog codes to be able to solve the path
count problem the `rect’ up to rect(7, 7). See below time statistics. The codes
uses my ZDD library. I have’t seen such other codes in prolog for the specific
problem.

I have used no other strategy than using matrixes over path sets in the grid
graph of the rect(N, M). Eeach element of the matrix has a set of paths in ZDD
structure, which is not new and might be seen in the literature on elementary
graph theory. I have little knowldge on algorithm for path counting
problems. As a fact, the codes uses only the library term_hash and vectors,
as the table/1 library. Without any help from others in futre, I can not go
further, I will wait until some unseen idea for me will luckily fall on me,
which, however, will not be the case probably.

?- time(zdd(count_by_bridge(rect(5, 5), C))).
 % 17,163,159 inferences, 2.033 CPU in 2.092 seconds (97% CPU, 8441057 Lips)
 C = 1262816 .

?- time(zdd(count_by_bridge(rect(6, 6), C))).
 % 86,167,536 inferences, 10.821 CPU in 10.978 seconds (99% CPU, 7963169 Lips)
 C = 575780564 .

?- time(zdd(count_by_bridge(rect(7, 7), C))).
 % 417,159,926 inferences, 61.951 CPU in 62.331 seconds (99% CPU, 6733754 Lips)
 C = 789360053252 .

?- time(zdd(count_by_bridge(rect(8, 8), C))).  % << stack overflow.

IMO, through this experience, I think ZDD library is useful also for Prolog
mostly because ZDD programming is declarative in nature, based on clear
semantics of operations over family of sets. It seems to have a complematry role
to list in Prolog. I hope someone share this feeling with me.

Kuniaki Mukai

10

I have found that my ZDD library is already able to make refutation in (ground)
propositional calculus. i.e., SAT. In fact,the ltr_refute/1 below is a
complete and very fast such a procedure. The other necessary codes are in my
pack pac misc/zdd.pl. I said most of the zdd.pl codes are junk, but codes
related to clauses of literals may not be junk, I hope. Also I would like to
update the pack/pac for those who might be interested in ZDD programming in
SWI-Prolog.

?- zdd((X<<dnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))),
	psa(X), ltr_refute(X))).
 [-a,b,-c]
 [a,-b,c]
 X = 19.
%
ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(false, _):-!.
ltr_refute(X, S) :- integer(X),
	cofact(X, if(A, L, R), S),
	(	R == true -> true
	;	R == false -> Y = L
	;	cofact(R, if(B, L0, R0), S),
		(	B == -(A)
		->  dnf_merge(L, L0, L1, S),
			dnf_join(R, R0, R1, S),
			dnf_join(L1, R1, Y, S)
		;	dnf_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).

Kuniaki Mukai

11

Sorry, codes sent appears corrupted. I reposts the codes.

?- zdd((X<<dnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))),
	psa(X), ltr_refute(X))).
 [-a,b,-c]
 [a,-b,c]
 X = 19.

%
ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(false, _):-!.
ltr_refute(X, S) :- integer(X),
	cofact(X, if(A, L, R), S),
	(	R == true -> true
	;	R == false -> Y = L
	;	cofact(R, if(B, L0, R0), S),
		(	B == -(A)
		->  dnf_merge(L, L0, L1, S),
			dnf_join(R, R0, R1, S),
			dnf_join(L1, R1, Y, S)
		;	dnf_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).

Kuniaki Mukai

12

Sorry again. I remember that dnf( disjunctive normal form) must be cnf(conjunctive normal form) in refutation procedure.

Correction.

% ?- spy(ltr_refute), zdd((X<<cnf(((a + b)*(a + -c)*(-a + c)*(-a + -b))),
%	psa(X), ltr_refute(X))).
%@ [-a,c]
%@ [-a,-b]
%@ [a,-c]
%@ [a,b]
%@  * Call: (18) zdd:ltr_refute(16) ? no debug
%@ X = 16.

ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(false, _):-!.
ltr_refute(X, S) :- integer(X),
	cofact(X, if(A, L, R), S),
	(	R == true -> true
	;	R == false -> Y = L
	;	cofact(R, if(B, L0, R0), S),
		(	B == -(A)
		->  cnf_merge(L, L0, L1, S),
			cnf_join(R, R0, R1, S),
			cnf_join(L1, R1, Y, S)
		;	cnf_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).

Kuniaki Mukai

13

The content you are adding is nice to see. Look forward to seeing more.

I notice that you have been making changes and starting a new reply each time. Perhaps you might do what others do and add a Edit header (example) and then the new information, e.g.

Edit 08.02.2020:

Updated information.

Also if your post are getting long, consider using Expandable text sections :slightly_smiling_face:

14

Edit 13.02.2020:

I have tested my refutation based prover in ZDD for the first-order (classical)
propositional logic. Although this is a toy test, the prover might be very
fast for larger formula thanks to representation of a set of clauses in ZDD.

Also correctness and completeness are obvious, by induction on the number of
literals. If I do not miss semething basic (though highly possible), this prover
is surely a rediscovery, because in general mechanical theorem prover has long and
strong tradition both in theory and practice. It is hard to imagine they missed
to use ZDD like structure. Anyway, as for a hobbist like me, it is enough that
ZDD programming is interesting also as a prolog programming method. In fact, so
far I have met several ZDD specific, I think, programming techniques or
patterns. I wish I have time to introduce them here soon when I am sure they
works correctly.

valid_formula(-(-a)->a).
valid_formula(a -> a).
valid_formula(a -> (b -> a)).
valid_formula((a->b)->((b->c)->(a->c))).
valid_formula(a->((a->b)->b)).
valid_formula((a*(a->b))->b).
valid_formula((a->b)->(-b -> -a)).
valid_formula((a->b)->((b->c)->(a->c))).

Here is a log of the test and codes of the prover. I hope
no serious bug in them.

% ?- time(forall(valid_formula(A), prove_by_refutation(A))).
%@ VALID.
%@ VALID.
%@ VALID.
%@ VALID.
%@ VALID.
%@ VALID.
%@ VALID.
%@ VALID.
%@ % 9,412 inferences, 0.001 CPU in 0.001 seconds (98% CPU, 13503587 Lips)
%@ true.

non_valid_formula(a).
non_valid_formula((a->b)->a).
non_valid_formula((a->b)->(b->a)).
non_valid_formula(a -> (b -> c)).

% ?- time(forall(non_valid_formula(A), prove_by_refutation(A))).
%@ NOT VALID.
%@ NOT VALID.
%@ NOT VALID.
%@ NOT VALID.
%@ % 4,252 inferences, 0.000 CPU in 0.001 seconds (96% CPU, 8642276 Lips)
%@ true.

%
prove_by_refutation(X):- expand_boole_macro(X, X0),
	zdd((boole_to_cnf(X0, X1),
		ltr_complement_toplevel(X1, X2),
		dnf_to_cnf(X2, X3),
		(	ltr_refute(X3)
		->  writeln('NOT VALID.')
		;	writeln('VALID.')
		))).
%
ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(true, _):-!.
ltr_refute(X, S) :- integer(X),
	cofact(X, if(A, L, R), S),
	(	R == true	-> true
	;	R == false	-> Y = L
	;	A = -(_)
	->	(	L == true	-> Y = R
		;	cnf_join(L, R, Y, S)
		)
	;   cofact(R, if(B, L0, R0), S),
		(	B == -(A)
		->  cnf_merge(L, L0, L1, S),
			cnf_join(L1, R0, Y, S)
		;	L==true
		->  Y = R
		; 	cnf_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).
1 Like
15

Thank you for kind advice, though still I don’t know how to do with “EDIT”.
Is my last post with “EDIT” what you had in mind to give me the advice ?

Kuniaki Mukai

1 Like
16

Since the post prior to the last was an accepted answer,

image
it is hard to know what that really meant.

In case you are not aware of how to edit a post at the bottom of an existing post you create will be

image

by clicking on the ellipsis ... you should see

image

The pencil will let you edit an existing post.

image

When you click on it you will bring up an editor window with the current text and a preview just to the right of it. From there it is like normal editing.

If you have any doubts about what to do, just do what you have been doing. With admin rights I can combine them if it clear the next post is an edit of the previous post. :slightly_smiling_face:

17

I changed the formatting of the code by changing

<pre>

</pre>

to

```prolog

```

See: Markdown help :slightly_smiling_face:

18

reply > elipsis > pacil I got it, thanks.

Kuniaki

1 Like
19 
Thank you very much.

Kuniaki