Toward ZDD library in SWI-Prolog

Announce Pack
1

I have made some improvements, I believe, on ZDD in prolog,
compared with my previsous versions. For example
I found a way to count boolean solutions of disjunctive
normal forms in ZDD. Tiny examples follows, which also the reader
could run. The predicate ltr_card below is what I happened to
find, among others, on considering what 0/1 in ZDD means.
I would like to hear whether the queries runs as following logs.

% swipl
?- pack_install(pac).
(`pac' installed @1.5.4 )
?- use_module(library(pac)).
?- use_module(zdd(zdd)).
?- module(zdd).
zdd:  ?- zdd((boole_to_dnf(a, X), ltr_card(1, X, C))).
X = 2,
C = 1.

zdd:  ?- zdd((boole_to_dnf(a+b, X), ltr_card(2, X, C))).
X = 4,
C = 3.

zdd:  ?- zdd((boole_to_dnf(-(a+b), X), ltr_card(2, X, C))).
X = 8,
C = 1.

zdd:  ?- zdd((boole_to_dnf((a+b)*(b+c), X), ltr_card(3, X, C))).
X = 10,
C = 5.

zdd:  ?- zdd((boole_to_dnf(-((a+b)*(b+c)), X), ltr_card(3, X, C))).
X = 18,
C = 3.

zdd:  ?-

ltr_card(N, X, Y):- shift(ltr_card(N, X, Y)).
%
ltr_card(N, X, Y, S):- setup_call_cleanup(
	open_memo(M),
	ltr_card(N, X, Y, S, M),
	close_memo(M)).

%
ltr_card(_, 0, 0, _,  _):-!.
ltr_card(N, 1, C, _,  _):-!, C is 2^N.
ltr_card(N, I, C, S, M):- zmemo(path_count(N, I)-C, M),
	(	nonvar(C) -> true
	;	cofact(I, t(A, L, R), S),
		N0 is N-1,
		(	L > 1,
			cofact(L, t(B, _, _), S),
			complementary(A, B)
		->	N1 is N
		;	N1 is N0
		),
		ltr_card(N1, L, Cl, S, M),
		ltr_card(N0, R, Cr, S, M),
		C is Cl + Cr
	).

Kuniaki Mukai

1 Like