Toward ZDD library in SWI-Prolog

As always, interesting work… but maybe you alter somewhat in strange ways the module search path ? After loaded library(pac), I’m unable to edit any files with PCEMACS

?- [library(pac)].
true.

?- edit(inv).
% Waiting for editor ... sh: 1: emacsclient: not found

% Editor returned failure; skipped make/0 to reload files
true.

I am not familiar with pack-install, but, I have found that it installs the package at
~/.local/share/swi-prolog/pack/pac

Kuniaki Mukai

A moment before, I have made an experiment on ZDD in Prolog after Jon Burse.
Although I am not familiar with the problem and don’t know much about
consequences of solving the probolem. The predicate jburse/2 below is a
modificatio of Jan Burse’s original problem. I remember a query as for original
jburse(8, C) took more than 24 hours at that time, while the current query
jburse(11, C) takes, surprisingly, 0.16 seconds. Moreover even jburse(50, C)
takes less than 8 seconds. Unfortunately I don’t know the answers are correct,
but I take these statistics as a sympton that ZDD is powerful for representing
sets of clauses of literals for logical manipulation. I would like to see more
symptons for this, though I have not appropriate samples to try for the moment.

% ?- time(jburse(11, C)).
%@ % 214,911 inferences, 0.016 CPU in 0.016 seconds (100% CPU, 13089962 Lips)
%@ C = 36028797018963968.
% ?- time(jburse(12, C)).
%@ % 271,012 inferences, 0.021 CPU in 0.022 seconds (97% CPU, 12645203 Lips)
%@ C = 73786976294838206464.
% ?- time(jburse(50, C)).
%@ % 65,606,276 inferences, 7.624 CPU in 7.747 seconds (98% CPU, 8604897 Lips)
%@ C = 57775629806269263488289979632051482575456970143627537546788321689581
513827390414894737077587573837927039774952943546092406410331900465187683013
127438054872058859787239344487340526509142954922629137112347328885171358590
506482657993919463409373750485918576896201055208715726777463241068425826712
1287728707126733386345748295699714571521040271552753678267463143641875218432.
%
jburse(N, C):-  N2 is N*N,
		jburse_grounded(N, P),
		zdd(( boole_to_dnf(P, Z), ltr_card(N2, Z, C))).
%
jburse_grounded(N, P):- problem(N, P),
	term_variables(P, Vs),
	length(Vs, Len),
	Len0 is Len + 1,
	numlist(2, Len0, Ns),
	Vs = Ns.

Kuniaki Mukai

It was a faithful translation of your problem, I thought.
Anyway I thank you, it was more than a couple years ago, and
I will not go into further.

?- listing(problem).

should show listings such like this.

% by Jan Burse. For testing %
problem(N, P):- matrix(N, M), constraint(M, P).
%
burse(N, P):- matrix(N, M), constraint(M, P).
%
matrix(N, M):- length(M, N), maplist(col(N), M).
%
col(N, L):- length(L, N).
%
inner_product([X], [Y], X*Y):-!.
inner_product([X|Xs], [Y|Ys], #((X*Y),Z)):- inner_product(Xs, Ys, Z).
%
constraint([V], E=:=true):- !, inner_product(V, V, E).
constraint([V|Vs], (E=:=true)*C*D):- inner_product(V, V, E),
constraint(Vs, D),
inner_constraint_one(V, Vs, C).
%
inner_constraint_one(V, [U], C=:=false):- !, inner_product(V, U, C).
inner_constraint_one(V, [U|Us], (C=:=false)*D):-
inner_product(V, U, C),
inner_constraint_one(V, Us, D).

I am sorry I am already too busy for old problems to spend time
for new proposed ones.

Kuniaki Mukai

You can check whether your algorithm is correct, when you compute
some small count numbers. And check against the count numbers that
were computed in the past.

If the numbers are the same, chances are high that your algorithm
is correct. If the numbers are not the same, then there is either a
bug in the old algorithm or in your new algorithm or in both.

As your post says, N=8 was already difficult in the past. Now you
show N=11, so how do you expect to verify that result?

Is it too fast ? I partially agree. Also I don’t remember
answers retuned by my old version. I lost old codes. Are answers below different
from yours for n =< 8 ? There might be bug(s) in my new
codes. I have to take time to review it,

% ?- forall(between(1, 10, N),
% ( jburse(N, C),
% writeln(jburse(N, C))
% )).
%@ jburse(1,1)
%@ jburse(2,2)
%@ jburse(3,8)
%@ jburse(4,64)
%@ jburse(5,1024)
%@ jburse(6,32768)
%@ jburse(7,2097152)
%@ jburse(8,268435456)
%@ jburse(9,68719476736)
%@ jburse(10,35184372088832)
%@ true.

Kuniaki Mukai

I found a serious logic bug in the ltr_card (counting solutions for DNF),
and have fixed it. Then the following query again. The result is still surprising.
I have no idea how to verify this result. As once I had hard time on this problem
to improve time efficiency, I can not believe the drastic current speed. However it is possible
that the codes is correct in some unexpected way.
Anyway I take time for a while for cooling down.

% ?- time(forall(between(1, 20, N),
%			( jburse(N, C),
%			  writeln(jburse(N, C))
%			))).
%@ jburse(1,1)
%@ jburse(2,2)
%@ jburse(3,8)
%@ jburse(4,64)
%@ jburse(5,1024)
%@ jburse(6,32768)
%@ jburse(7,2097152)
%@ jburse(8,268435456)
%@ jburse(9,68719476736)
%@ jburse(10,35184372088832)
%@ jburse(11,36028797018963968)
%@ jburse(12,73786976294838206464)
%@ jburse(13,302231454903657293676544)
%@ jburse(14,2475880078570760549798248448)
%@ jburse(15,40564819207303340847894502572032)
%@ jburse(16,1329227995784915872903807060280344576)
%@ jburse(17,87112285931760246646623899502532662132736)
%@ jburse(18,11417981541647679048466287755595961091061972992)
%@ jburse(19,2993155353253689176481146537402947624255349848014848)
%@ jburse(20,1569275433846670190958947355801916604025588861116008628224)
%@ % 9,061,329 inferences, 0.674 CPU in 0.727 seconds (93% CPU, 13436672 Lips)
%@ true.

Kuniaki Mukai

1 Like

Didn’t you provide a pack before? Should be possible to retrieve that, no?

Thank you for your kind proposal, but
I saw a fragment of log in my local git like this:

?- time(continue((problem(7, P), solc(P, X)))).
%@ % 366,853,945 inferences, 94.389 CPU in 96.556 seconds (98% CPU, 3886607 Lips)
%@ X = 1451520.

I am still not good at GIT. I wish I could grep on all commits in my local repository, for example.

On the other hand, this is a log by the new version with
boole_to_dnf + ltr_card, where “everything” is done simply in ZDD.

% ?- time(jburse(7, C)).
38,378 inferences, 0.004 CPU in 0.004 seconds (84% CPU, 10269735 Lips)
%@ C = 2097152.

The difference suggests that there are bugs in even both of
my two codes. However, as I don’t know the correct answer yet, and
the new version works correctly so far for all test cases
including on propostional logic which I prepared, I will take care of
the new codes only. I will appreciate bug reports.

Kuniaki Mukai

I have found that what the predicate jburse produces is reproduced
by another simple way below. It is interesting that the original problem
by Jan Burse has this property. I will be happy if it is the case because
it supports correctness of my ZDD toward a SWI-Prolog package.

% ?- forall( between(1, 20, I),
%			(	f(I, P),
%				X is 2^P,
%				writeln((2^f(I)=2^P)=X)
%			)).

%@ (2^f(1)=2^1)=2
%@ (2^f(2)=2^3)=8
%@ (2^f(3)=2^6)=64
%@ (2^f(4)=2^10)=1024
%@ (2^f(5)=2^15)=32768
%@ (2^f(6)=2^21)=2097152
%@ (2^f(7)=2^28)=268435456
%@ (2^f(8)=2^36)=68719476736
%@ (2^f(9)=2^45)=35184372088832
%@ (2^f(10)=2^55)=36028797018963968
%@ (2^f(11)=2^66)=73786976294838206464
%@ (2^f(12)=2^78)=302231454903657293676544
%@ (2^f(13)=2^91)=2475880078570760549798248448
%@ (2^f(14)=2^105)=40564819207303340847894502572032
%@ (2^f(15)=2^120)=1329227995784915872903807060280344576
%@ (2^f(16)=2^136)=87112285931760246646623899502532662132736
%@ (2^f(17)=2^153)=11417981541647679048466287755595961091061972992
%@ (2^f(18)=2^171)=2993155353253689176481146537402947624255349848014848
%@ (2^f(19)=2^190)=1569275433846670190958947355801916604025588861116008628224
%@ (2^f(20)=2^210)=1645504557321206042154969182557350504982735865633579863348609024
%@ true.

where,
f(1) = 1.
f(n) = f(n-1) + n.

f(1, 1):-!.
f(N, X):- N>1,
	N0 is N-1,
	f(N0, X0),
	X is X0 + N.

Kuniaki Mukai

Here is an expereiment on ZDD, which might be interesting for the discourse.
It is easy to build such a (big) set F of clauses of literals in ZDD

  1. F has N varialbles. (N: given).
  2. F is valid as DNF.
  3. F is unsatisifiable as CNF.

By 2 the number of solutions of F should be 2^N. By 3 a refutation for F should succeed.

In fact, as log below, predicate ltr_refute below for F succeeds, and ltr_card for F returns 2^N.

Time statisics sounds to say: counting is much faster than refutation. Of course my current codes of ltr_refute is so simple and naive as the source codes listing below. Sadly, I have no idea how to improve codes. Anyway although ZDD implementation of mine is based on my simple-minded background on ZDD, I have already shown up, I hope, that some advertised powerful features of ZDD is possible in SWI-Prolog in small prolog codes.

The current version of the pack pac is 1.5.6. After pack_install the pac, the following log shoud be reproduced:

% ?- use_modul(library(pac)).
% ?- use_modul(zdd(zdd)).
% ?- module(zdd).
% ?- time(zdd((a_big_cnf(100, X), ltr_card(100, X, C)))), C =:= 2^100.
%@ % 2,392,546 inferences, 0.290 CPU in 0.409 seconds (71% CPU, 8246121 Lips)
%@ X = 30001,
%@ C = 1267650600228229401496703205376 .
% ?- call_with_time_limit(100, time(zdd((a_big_cnf(30, X), ltr_refute(X))))).
%@ % 123,551,444 inferences, 14.271 CPU in 14.439 seconds (99% CPU, 8657765 Lips)
%@ X = 2701.
a_big_cnf(X, Y):- shift(a_big_cnf(X, Y)).
a_big_cnf(0, 1, _).
a_big_cnf(N, X, S):- N>0,
	N0 is N-1,
	a_big_cnf(N0, X0, S),
	ltr_insert(N, X0, R, S),
	ltr_insert(-N, X0, L, S),
	zdd_join(L, R, X, S).
% refutation by resolution in ZDD.
ltr_refute(X):- shift(ltr_refute(X)).
%
ltr_refute(X, S) :- zdd_has_empty(X, S), !.
ltr_refute(X, S) :- X > 1,
	cofact(X, t(A, L, R), S),
	(	L = 0  -> Y = R
	;	cofact(L, t(B, L0, R0), S),
		(	B = -(A)
		-> 	ltr_merge(R0, R, Y0, S),
			ltr_join(L0, Y0, Y, S)
		;   ltr_join(L, R, Y, S)
		)
	),
	ltr_refute(Y, S).

family_card/2 below classifies a given family of sets by cardiality.
The log below is for the powerset of a set U = [1,2,3,…,1000],
and shows the number of subsets of U which has 500 elements.
I think that time 10.355 CPU in 10.540 seconds is reasonable
as for ZDD in SWI-Prolog. The codes below contains reduntant in my sence
because I see multiple time term_hash calll in a redundant way, but
I am almost new for this subttle thing on programming, and busy enough
only for naive version.

% ?- N = 1000, numlist(1, N, Ns),
%	time(zdd((X<<pow(Ns), family_card(X, P),
%	zmemo(family_with_card(500)-L), card(L, C)))).

%@ % 90,174,772 inferences, 10.355 CPU in 10.540 seconds (98% CPU, 8708585 Lips)
%@ C = 270288240945436569515614693625975275496152008446548287007392875106625428705522193898612483924502370165362606085021546104802209750050679917549894219699518475423665484263751733356162464079737887344364574161119497604571044985756287880514600994219426752366915856603136862602484428109296905863799821216320.
% Classify sets in a family by cardinality.

%
max(A, B, A):- A@>B, !.
max(_, B, B).

family_card(X, Y):- shift(family_card(X, Y)).
%
family_card(0, 0, _):-!.
family_card(1, 0, S):-!, zmemo(family_with_card(0)-1, S).
family_card(I, P, S):- zmemo(family_card_done(I)-B, S),
	(	nonvar(B) ->  true
	; 	cofact(I, t(A, L, R), S),
		family_card(L, Pl, S),
		family_card(R, Pr, S),
		max(Pl, Pr, P0),
		insert_one_to_family(A, P0, New, S),
		P is P0 + 1,
		zmemo(family_with_card(P)-New, S),
		B = true
	).
%
insert_one_to_family(A, 0, G, S):-!, zmemo(family_with_card(0)-F, S),
	insert_atom(A, F, G, S).
insert_one_to_family(A, P, G, S):- P0 is P-1,
	insert_one_to_family(A, P0, G0, S),
	zmemo(family_with_card(P)-Fp, S),
	insert_atom(A, Fp, G, S),
	zdd_join(Fp, G0, Gp, S),
	set_memo(family_with_card(P)-Gp, S).

Kuniaki Mukai

The specker problem is interesting, since it is related to my orthogonal boolean vector problem. But I am still kind at beginning of solving it, since I dont have super computer in my back yard.

The specker paper has a solution based on orthogonal vectors. I came up with orthogonal boolean vector problem (the problem/2 in kuniaki mukais code) because of the specker problem.

So its not really a new problem what I am asking here. But to understand the context of the relation c(_,_) and operation _+_ you probably need to read the Kochen-Specker paradox paper.

Thank you advice for checking the Kochen-Specker paradox paper. It is impressive that
your problem on orthogonal vectors is related to the paper, though I know nothing about the Kochen-Specker paradox. I will check it later.

Unfortunately, I am busy for a couple of programming on ZDD. One is on path counting of a grid graph ( Minato group solved for grid nodes {(x,y) | 1=<x,y=<N } N=< 21 ?? about 10 years ago based on SimPath method by D.Knuth. I know little on this.) The other is related counting a single sorted associative algebra with a given cardinality. On both of them I have only miserable failure history in my life as challage for “Prolog programming” in my sense. Still I can’t expect much about my ZDD implementation, but anyway I would like to post something here on experiment results soon.

Kuniaki Mukai

Yes counting or how it is sometimes called sharp-SAT written as #SAT can be also used for satisfiability. Its very simple a formula is satisfiable if and only if the satisfiability count is non zero.

But I did only counting in the orthogonal base problem because I wanted to see how many bases there are in case I would need to filter them to solve the specker problem and how much work this would cause.

But the more decisive solution to the specker problem would be to not only count solution but to actually exhibit a solution. Thats kind of solving the why problem of explanable artificial intelligence.

The inovation of the Specker Kochen paradox is its finite counter model.

See also:

The Kochen-Specker theorem in quantum mechanics
https://www.researchgate.net/publication/251880832

About the problem of counting associative algebras on a domain D, I have run two versions of codes to get the following results. One, say A, is using ZDD, the other, say B, is not. For |D|=1, 2, 3, A and B returns 1, 8, 113, respectively. For |D|=4, A returns 3492, but B got “timeout.” As the number of algebras on D are 1, 2^4, 3^9, 4^{16}, 5^{25}, \ldots for |D|= 1, 2, 3, 4, 5, \ldots, respectively, the current results should be acceptable, I think. I naively expected on beginning the experiment that there might be some idea on ZDD to use its property of rich structure sharing, but I could not find them. Thus, both codes are naive and brute force. I will appreciate for any pointer to this counting problem. I’m amateur on counting problem in general.

Query log.
% ?-zdd(( count_associative_algebra_with_zdd(1, C))).
%@ C = 1.

% ?-zdd(( count_associative_algebra_with_zdd(2, C))).
%@ C = 8.

% ?-time(zdd(( count_associative_algebra_with_zdd(3, C)))).
%@ % 426,394 inferences, 0.074 CPU in 0.074 seconds (100% CPU, 5789228 Lips)
%@ C = 113.

% ?-time(zdd(( count_associative_algebra_with_zdd(4, C)))).
%@ % 143,325,850 inferences, 25.723 CPU in 25.729 seconds (100% CPU, 5571848 Lips)
%@ C = 3492.

% ?-call_with_time_limit(1800, zdd(( count_associative_algebra_with_zdd(5, C)))).
%@ ERROR: Unhandled exception: Time limit exceeded
Codes using ZDD.
count_associative_algebra_with_zdd(N, C):-
	prepare_count_associative_algebra(N, Track, Etree),
	count_assoc_algebras([h(Etree, [], Track)], 0, C).
%
prepare_count_associative_algebra(N, Track, Etree):-
	numlist(1, N, Dom),
	raise_list(Dom, 2, Dom2),
	product_list(Dom, Dom2, Dom3),
	maplist(pred([U, a(U, [], [])]), Dom3, Track),
	zdd:map_space(Dom2, Dom, Etree, equational_mapsto).

%
count_assoc_algebras(X, Y, Z):- shift0(count_assoc_algebras(X, Y, Z)).

%
count_assoc_algebras([], C, C, _).
count_assoc_algebras([h(0, _, _)|Hs], C, C0, S):-!,
	count_assoc_algebras(Hs, C, C0, S).
count_assoc_algebras([h(_, _, 0)|Hs], C, C0, S):-!,
	count_assoc_algebras(Hs, C, C0, S).
count_assoc_algebras([h(1, _, [])|Hs], C, C0, S):-!, C1 is C+1,
	count_assoc_algebras(Hs, C1, C0, S).
count_assoc_algebras([h(1, _, _)|Hs], C, C0, S):-!,
	count_assoc_algebras(Hs, C, C0, S).
count_assoc_algebras([h(Etree, Es, Tr)|Hs], C, C0, S):-
	cofact(Etree, t(E, L, R), S),
	repeat_law([E|Es], Tr, Tr0),
	(	Tr0 = 0
	->	count_assoc_algebras([h(L, Es, Tr)|Hs], C, C0, S)
	;	count_assoc_algebras([h(L, Es, Tr), h(R, [E|Es], Tr0)|Hs], C, C0, S)
	).

I tried ordinal codes without using ZDD.

Query without using ZDD.
% ?- count_associative_algebra(1, X).
%@ X = 1.

% ?- count_associative_algebra(2, X).
%@ X = 8.

% ?- time(count_associative_algebra(3, X)).
%@ % 87,217,314 inferences, 15.452 CPU in 15.477 seconds (100% CPU, 5644233 Lips)
%@ X = 113.

% ?- call_with_time_limit(180, time(count_associative_algebra(4, X))).
%@ % 984,263,663 inferences, 157.935 CPU in 198.803 seconds (79% CPU, 6232073 Lips)
%@ ERROR: Unhandled exception: Time limit exceeded
Codes without using ZDD.
count_associative_algebra(N, NumOfAssocAlgebras):-
	numlist(1, N, Dom),
	raise_list(Dom, 2, Dom2),
	product_list(Dom, Dom2, Dom3),
	maplist(pred([U, a(U, [], [])]), Dom3, Track0),
	sort(Track0, Track1),
	map_space_in_list(Dom2, Dom, Maps),
	maplist(maplist( pred([[A,B]-C, A+B=C]) ), Maps, FamEs),
	foldl( pred(Track1, (	[Es, C, C0]	:-
							repeat_law(Es, Track1, Track),
							(		Track = [] -> C0 is C+1
							;		C0 = C
						    ))
					   ),
		   FamEs,  0,  NumOfAssocAlgebras).

% ?- N is 3, M is 3, time(( numlist(1, N, X), numlist(1, M, Y),
%	map_space_in_list(X, Y, F), length(F, C))).
%
map_space_in_list([], _, [[]]).
map_space_in_list([X|Xs], Y, Z):- map_space_in_list(Xs, Y, Z0),
	map_space_in_list(Y, X, Z0, Z, []).
%
map_space_in_list([], _, _, Z, Z).
map_space_in_list([Y|Ys], X, Z, U, V):-
	fold_map_extend(Z, Y, X, U, U0),
	map_space_in_list(Ys, X, Z, U0, V).
%
fold_map_extend([], _, _, U, U).
fold_map_extend([Z|Zs], Y, X, [[X-Y|Z]|U], V):-
	fold_map_extend(Zs, Y, X, U, V).

Common predicates for checking assoiciative law.
%
repeat_law(E, [a(_,[A],[A])|X], Y):-!, repeat_law(E, X, Y).
repeat_law(_, [a(_,[_],[_])|_], 0):-!.	% 0 means NON Associativitty.
repeat_law(Eqs, X, X0):- member(E, Eqs),
	apply_law_once(E, X, X1),
	!,
	repeat_law(Eqs, X1, X0).
repeat_law(_, X, X).

%
apply_law_once(E, X, [A0|X0]):-
	select(A, X, X0),
	law(E, A, A0).

% law/3
law( A+B=C,	a([X, A, B], U, []),
			a([X, A, B], U, [X, C])).
law( A+B=C,	a(T, U, [A, B]),
			a(T, U, [C])).
law( A+B=C,	a(T, [A, B], U),
			a(T, [C], U)).
law( A+B=C,	a([A, B, X], [], U),
			a([A, B, X], [C, X], U)).

Kuniaki Mukai

There is something wrong in your formula, I get:

?- X is 3^9.
X = 19683

Which is quite different from 113.

3^9 is the number of algebras on \{1,2,3\}. 113 is the number of associative algebras on {1, 2, 3}.

Kuniaki Mukai

Ok, I could use sat_count/2 from SWI-Prolog CLP(B) to verify:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

?- ['/Projects/Jekejeke/Prototyping/experiment/other/diffuse3/finite/maze/kuniaki.pl'].
true.

?- time(test_many).
1
D = 1
% 1,466 inferences, 0.001 CPU in 0.013 seconds (5% CPU, 2130814 Lips)
true ;
8
D = 2
% 85,348 inferences, 0.106 CPU in 0.198 seconds (54% CPU, 807119 Lips)
true ;
113
D = 3
% 367,363,924 inferences, 44.804 CPU in 45.834 seconds (98% CPU, 8199276 Lips)
true .

I just use my model finder with the axiom:

axiom('associativity',
   all(X,all(Y,all(Z,X+(Y+Z)=(X+Y)+Z)))).

And a false conclusion. Will upload code to gist as soon as I am at another computer.

Have uploaded your challenge to gist:

Updated version of Model Finder, now supports also counting models
https://gist.github.com/jburse/213823a3ee93227147aad15321864190#file-picker2-pl

Number of Associative Algebras
https://gist.github.com/jburse/213823a3ee93227147aad15321864190#file-kuniaki-pl

Interstingly my CLP(B) cannot go that far, for my CLP(B) I only get:

Jekejeke Prolog 4, Runtime Library 1.4.6

?- test_many.
1
D = 1
Yes ;
8
D = 2
Yes ;
Error: Execution aborted since memory threshold exceeded.
	sat_count/2
	falsify_many/3
	test_many/0

So this could be some test case to work on an improved CLP(B) that
is less resource hungry. Also SWI-Prolog cannot go beyond D=3 for this example,
at least I wasn’t patient enough to await a solution for D=4.

Can you solve the Kochen Specker problem? It seems your ZDD can count even D=4 for associative algebras. Where as my CLP(B) and SWI-Prolog CLP(B) are chocking on D=4. My CLP(B) can even not do D=3 and SWI-Prolog, I did abort it after one minute.

Associative algebras has this constraint:

axiom('associativity',
   all(X,all(Y,all(Z,X+(Y+Z)=(X+Y)+Z)))).

The Kochen Specker problem is just another set of constraints together with a falsified conclusion:

axiom('reflexive compatibility', all(X,c(X,X))).
axiom('symmetric compatibility', all(X,all(Y,(c(X,Y)-:c(Y,X))))).
axiom('partial commutativity',
   all(X,all(Y,(c(X,Y)-:X+Y=Y+X)))).
axiom('partial associativity',
   all(X,all(Y,all(Z,(c(X,Y),c(X,Z),c(Y,Z)-:X+(Y+Z)=(X+Y)+Z))))).
case(2, 'leibniz formula',
   all(X,all(Y,(c(X,Y)-:all(Z,(c(X,Z),c(Y,Z)-:all(T,(c(X,T),
       c(Y,T),c(Z,T)-:(X+Y)+(Z+T)=(X+Z)+(Y+T))))))))).

What I don’t understand from your ZDD code that you posted, how you
represent model constraints, and whether you have some way to formulate
them as FOL as I did above. Your " Common predicates for checking assoiciative law"

looks quite cryptic and manually created. Would it be possible to have a FOL
input to your ZDD? So that from a FOL (First Order Logic) formulation a finite
model is searched?