Is there a way to control tabling for functional predicates with very large argument as computation state

Here is a favorite query sample on zdd programming. It works
for a set Ns of cardinality 10000 to enumarate the power set of Ns.
I’s fast enough, I think.

% ?-N = 10000,  numlist(1, N, Ns), time((zdd X<<pow(Ns), card(X, _C))), _C=:= 2^N.
%@ % 1,298,553 inferences, 0.105 CPU in 0.114 seconds (92% CPU, 12364110 Lips)
%@ N = 10000,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = 10001.

As I dropped shit/reset control from my implementation of library(zdd),
I thought tabling should work on library(zdd). However, with the favorite sample above, query with tabling version was aborted with "not enough  resources" even for a smaller set of 1000 elements.

% ?- numlist(1, 1000, Ns), (zdd X<<pow(Ns), card(X, C)).
%@ ERROR: '$tbl_variant_table'/6: Not enough resources: private_table_space
%@ ^  Exception: (11,771) catch('$tabling':create_table(<trie>(0x6000009a91e0), fresh(105553147668960, 105553129533248), ret(_78667858, _78417278, _78417280, _78417282, _78417284, _78417286, _78417288, _78417290, _78417292, _78417294, _78417296, _78417298, _78417300, _78417302, _78417304, _78417306, _78417308, _78417310, _78417312, _78417314, _78417316, _78417318, _78417320, _78417322, _78227762, _78227764, _78227766, _78227768, _78452420, _78452422, _78452424, _78452426), zmod:card_with_memo(22, _78667858, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(22, _78667858, s(..), s(..)))), deadlock, '$tabling':restart_tabling(<closure>(zmod:card_with_memo/4), zmod:card_with_memo(22, _78667858, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(22, _78667858, s(..), s(..))))) ? creep
%@ ^  Exception: (11,759) catch('$tabling':create_table(<trie>(0x6000009a9130), fresh(105553147668880, 105553129533104), ret(_78667638, _78417278, _78417280, _78417282, _78417284, _78417286, _78417288, _78417290, _78417292, _78417294, _78417296, _78417298, _78417300, _78417302, _78417304, _78417306, _78417308, _78417310, _78417312, _78417314, _78417316, _78417318, _78417320, _78417322, _78227762, _78227764, _78227766, _78227768, _78452420, _78452422, _78452424, _78452426), zmod:card_with_memo(23, _78667638, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(23, _78667638, s(..), s(..)))), deadlock, '$tabling':restart_tabling(<closure>(zmod:card_with_memo/4), zmod:card_with_memo(23, _78667638, s(..), s(..)), zmod:call(<closure>(zmod:card_with_memo/4)(23, _78667638, s(..), s(..))))) ? abort
%@ % Execution Aborted

The source codes are listed below. I guess ‘not enough resources’ was due to large argument S of zdd_join/4 and likely also for others. Usually S is a big term including vector and hash tables which are
extented to that of doubled size iteratively. S keeps every information
for computation. However, as for zdd programming, S is mainly to keep the functional dependency. So S should be safely ignored as for tabling, I think.

There might be already described in the documntation how to control
tabling for such card/3 and zdd_join/4, though I have failed to find.

source code with tabling or memo
:- table zdd_join/4.
%
zdd_join(0, X, X, _):-!.
zdd_join(X, 0, X, _):-!.
zdd_join(X, X, X, _):-!.
zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, Y, Z, S):-
		cofact(X, t(A, L, R), S),
		cofact(Y, t(A0, L0, R0), S),
		zdd_compare(C, A, A0, S),
		(	C = (<)	->
 			zdd_join(L, Y, U, S),
			cofact(Z, t(A, U, R), S)
		;	C = (=)	->
			zdd_join(L, L0, U, S),
			zdd_join(R, R0, V, S),
			cofact(Z, t(A, U, V), S)
		;	zdd_join(L0, X, U, S),
			cofact(Z, t(A0, U, R0), S)
		).

%
card(X, Y, S):- setup_call_cleanup(
	open_state(M),
	card_with_memo(X, Y, S, M),
	close_state(M)).

:- table card_with_memo/4.
card_with_memo(I, I, _, _):- I < 2, !.
card_with_memo(I, C, S, M):- % memo(I-C, M),
		cofact(I, t(_, L, R), S),
		card_with_memo(R, Cr, S, M),
		card_with_memo(L, Cl, S, M),
		C is Cl + Cr.
Default: zdd_join/4, card/3 without tabling but with memo.

zdd_join(0, X, X, _):-!.
zdd_join(X, 0, X, _):-!.
zdd_join(X, X, X, _):-!.
zdd_join(1, X, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, 1, Y, S):-!, zdd_join_1(X, Y, S).
zdd_join(X, Y, Z, S):-
	(	X@<Y -> memo(zdd_join(X,Y)-Z, S)
	;	memo(zdd_join(Y, X)-Z, S)
	),
	(	nonvar(Z) -> true  %, write(.)
	;	cofact(X, t(A, L, R), S),
		cofact(Y, t(A0, L0, R0), S),
		zdd_compare(C, A, A0, S),
		(	C = (<)	->
 			zdd_join(L, Y, U, S),
			cofact(Z, t(A, U, R), S)
		;	C = (=)	->
			zdd_join(L, L0, U, S),
			zdd_join(R, R0, V, S),
			cofact(Z, t(A, U, V), S)
		;	zdd_join(L0, X, U, S),
			cofact(Z, t(A0, U, R0), S)
		)
	).

%
card(X, Y, S):- setup_call_cleanup(
	open_state(M),
	card_with_memo(X, Y, S, M),
	close_state(M)).

%
card_with_memo(I, I, _, _):- I < 2, !.
card_with_memo(I, C, S, M):- memo(I-C, M),
	(	nonvar(C) -> true
	;	cofact(I, t(_, L, R), S),
		card_with_memo(R, Cr, S, M),
		card_with_memo(L, Cl, S, M),
		C is Cl + Cr
	).

Have a happy new year 2024 !

In order to see whether my library(pac/zdd) 1.8.7 could be rewritten to that based on tabling (using table/1 directive), a global variable, say gvar, is introduced so that big term for computation state (mutable) is bound to gvar and the name gvar is passed around as argument of predicates, instead of the big state content. Details should be omitted here, though it was not difficult.

Test query is to enumerate elements of the powerset of a set Ns of 10,000 elements, and to count the cardinality of of the powerset, which is well-known to be 2^10000.

According to the test, existing memo/2 version is roughly 6 times faster than tabling one.

tabling		0.928 seconds CPU
memo/2		0.140 seconds CPU

Although this rough test might sound negative to rewrite the library(pac/zdd) for using tabling, The use of tabling seems right direction for library(pac/zdd) to go. Main reason is a smart syntax of tabling directive. It is often that use of memo/2 turns out not effective at all depending on a predicate, but in that case it is little bit cunbersome to erase lines related to use of memo/2 due to its block structure of effect of memo/2 as seen in the example.

memo/2 version
% ?- numlist(1, 10000, L), time((zdd X<< pow(L), card(X, C))).
%@ % 1,162,130 inferences, 0.140 CPU in 0.189 seconds (74% CPU, 8300039 Lips)
%@ L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = 10001,
tabling  by :- table(zdd_join/4), :- table(card_with_memo/4.
% ?- time((zdd X<<pow(:numlist(1, 10000)), card(X, _C))).
%@ % 1,172,154 inferences, 0.928 CPU in 1.684 seconds (55% CPU, 1263725 Lips)
%@ X = 10001.

It is not clear for me whether there is a way to use tabling other than introducing such global variable gvar for mutable possibly big state, not to pass around state contents directly as argument.

It is not entirely clear what is happening to me. Tabling assumes that the answers of a predicate are solely derived from its (input) arguments. Or, with incremental tabling, from dynamic predicates that are registered as incremental. If an argument does not contribute to the computation, simply create a version without this argument and table that.

You suggest that one of the predicate arguments is a term that is subject to destructive assignment. If that argument is used in the computation this can only work if it is global data similar to dynamic predicates and it does not change during the tabled computation. In addition, of the global data changes the user shall abolish the affected tables. If this is the situation, using a global variable is probably the best work-around.

If the term is ground, XSB has an option to “intern” a term, which implies the term is replaced by an atomic constant. SWI-Prolog doesn’t have, although global variables come close.

Tabling provides memorization as well as handling “left recursion” and better semantics (Well Founded Semantics) for negation. SWI-Prolog’s current implementation is based on the work by Benoit Desouter on tabling as a library on top of delimited continuations. It was turned into a fully functional version with help from Theresa Swift and David Warren from XSB, sponsored by Kyndi inc. Most of the admin was moved to C to get reasonable scalability and performance. Still, a significant amount of the time critical work is done in Prolog. To compete on performance, most of that should be moved into the VM.

(Nothing of importance)

How would you solve the problem of finding all paths between two nodes?

  • Is there a path between two nodes – tabling handles this.
  • What is the minimum path between two nodes – tabling handles this also, although it’s a bit inefficient because the path is tabled even though it isn’t used in the computation.

But: find a path between two nodes, and allow backtracking to other nodes … tabling can’t handle this.

This could be handled with tabling if it allowed a mode of “ignore this output parameter”. I had a discussion with David S Warren about adding this to XSB (this was before SWI-Prolog supported tabling) and he was opposed. Unfortunately, I don’t have a record of our discussion, but my recollection is that he opposed it because it could easily be abused in a “non-logical” way and I didn’t have a good response to his objection.

[I eventually found a different way of solving my problem that didn’t require finding all paths, so maybe this isn’t a problem that needs solving … although @kuniaki.mukai seems to require it for efficiency, and finding the minimum path would be more efficient if the “path” argument could be ignored.]

I see the point. Yes, the “state” argument is always updated in a destructive way as you guessed. I have checked that, fortunately it is easy to convert the current version to that which uses a global variable, and that state argument could be dropped from all application predicates. If access to global variable with b_setval/2 and b_getval/2 is marginally as efficient as that to arguments by the head unification, now there seems no reason to keep the argument place for the state.

I remember I thought a similar thing for commutative operations
(join, meet, merge, etc). Perhaps I disliked to have secondary names
for predicates.

Sounds interesting. I thought predicates which works as function,
tabling should work ignoring unrelated arguments. In other words,
tabling works, I thought, as an association lists which keep only input and output. Your post pushes me to learn how tabling works, and in particular, what is “well-founded semantics” of tabling.

card/3, for example, creates a working state only for
counting, which is closed when the job is completed.
States work almost as cache. The 4th parameter is needed to
to tell which “cache” to be used.

I have edited to get an experimental version of library(pac/zdd), in which state (mutable cache) is successfully hided from argument pleces of most of applications predicates on ZDD. As far as a small number of queries, performace seems rather a little bit more efficient than existing library(pac/zdd) 1.8.8, which I did not expected, and sounds strange. So I have to keep both branches until it will be clear on which version is better.

% ?- N = 10000, numlist(1, N, Ns),time( (zdd X<< pow(Ns), card(X, _C))),
%	_C =:= 2^N.
%@ % 1,388,541 inferences, 0.088 CPU in 0.106 seconds (83% CPU, 15731502 Lips)
%@ N = 10000,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ X = 10001.

card(X, Y):- setup_call_cleanup(
	open_memo,
	card_with_memo(X, Y),
	close_memo).
%
card_with_memo(I, I):- I < 2, !.
card_with_memo(I, C):- memo(zdd_card(I)-C),
	(	nonvar(C) -> true
	;	cofact(I, t(_, L, R)),
		card_with_memo(R, Cr),
		card_with_memo(L, Cl),
		C is Cl + Cr
	).

However, although tabling works on the experimental version efficiently, I have noticed that zdd_join(X, Y, Z), for instance, is locally works as function (X, Y) |-> Z, but it depends on states. X, Y, Z are always integer ids of families of sets. Consequently a sequence of untable(zdd_join/3), table(zdd_join/3) is necessarey when the meaning of integer arguments of zdd_join
might change.

% ?- N = 10000, numlist(1, N, _Ns),time( (zdd X<< pow(_Ns), table_card(X, _C))),
%	_C =:= 2^N.
%@ % 1,272,369 inferences, 0.098 CPU in 0.113 seconds (87% CPU, 12990383 Lips)
%@ N = 10000,
%@ X = 10001.

% ?- N = 10000, numlist(1, N, _Ns),time( (zdd X<< pow(_Ns), table_card(X, _C))),
%	_C =:= 2^N.
%@ % 852,340 inferences, 0.065 CPU in 0.070 seconds (93% CPU, 13075908 Lips)
%@ N = 10000,
%@ X = 10001.

:- table(table_card/2).
table_card(I, I):- I < 2, !.
table_card(I, C):-
	cofact(I, t(_, L, R)),
	table_card(R, Cr),
	table_card(L, Cl),
	C is Cl + Cr.

Anyway, I am expericing that b_getval/2 is suprisingly fast. It seems marginally as fast way as passing argument via the head unification.

Here is my first codes for ltr_xor/4 (exclusive-or ?) in zdd.
I’m not sure this could be an answer what is requested, but it is
all what I can do. ltr_negate/4 in the codes has been added
to library(pac/zdd) 1.8.8 as completion of handling clauses of literals
after a well-known meta logical rule in propositional logic something called duality law, I forgot the exact name.

% ?- ltr_zdd  X<<dnf(a+b), Y<<dnf(b+c), ltr_xor(X, Y, Z), psa(Z), ltr_card(Z, C).
%@  zid = 19
%@ 	[-a,-b,c]
%@ 	[a,-b,-c]
%@ -------------------
%@ X = 4,
%@ Y = 6,
%@ Z = 19,
%@ C = 2.

% ?- ltr_zdd  Z<< dnf((a+b)=\=(b+c)), psa(Z), ltr_card(Z, C).
%@  zid = 17
%@ 	[-a,-b,c]
%@ 	[a,-b,-c]
%@ -------------------
%@ Z = 17,
%@ C = 2.

% Assuming in DNF.  Z = xor(X, Y).
ltr_xor(X, Y, Z, S):-
	ltr_negate(Y, Y0, S),
	ltr_merge(X, Y0, U, S),
	ltr_negate(X, X0, S),
	ltr_merge(X0, Y, V, S),
	ltr_join(U, V, Z, S).

zdd_xor is on two farmilies of sets, but ltr_xor is on two DNF (two families of clauses. ) For example, ltr_merge(X, X, X, _) is forced to be true by idemopotent law of conjunction (merge), but zdd_merge(X, X, X, ) is not always true as for set operation.
BTW, I have noticed there is a bug that made it always true.
I removed the line of codes. It’s a kind of shameful bug. Thanks.

l took it as “remove negative literals from each clauses” like this

    {[-a], [b]} => {[], [b]}.

So, here is codes which might be some help, though it is not tested yet.

% ?- ltr_zdd X<< dnf(a->b), psa(X),
%	pred_remove_atoms(negative_literal, X, Y), psa(Y).
%@  zid = 4
%@ 	[b]
%@ 	[-a]
%@ -------------------
%@  zid = 5
%@ 	[]
%@ 	[b]
%@ -------------------
%@ X = 4,
%@ Y = 5.

negative_literal(-(_)).

:- meta_predicate pred_remove_atoms(1, ?, ?).

pred_remove_atoms(_, X, X):- X<2, !.
pred_remove_atoms(Pred, I, J):- memo(pred_remove(I)-J),
	(	nonvar(J)	->  true
	; 	cofact(I, t(A, L, R)),
		pred_remove_atoms(Pred, L, L0),
		pred_remove_atoms(Pred, R, R0),
		(	call(Pred, A) ->
			zdd_join(L0, R0, J)
		;	cofact(J, t(A, L0, R0))
		)
	).

I tried to wrap atomic goals with the use_table/1 to apply tabling on zdd programming.

use_table(G):- functor(G, F, N),
	setup_call_cleanup(
		table(F/N),
		G,
		untable(F/N)
		).

Overall result was that use_table (tabling) is still weaker than the imperative (and cumbersome) use of the existing ‘memo/1’, which is a little bit disappointed for me. The “imprative memo” version succeeded in a few seconds for the test.

The test was to factorize a big binary term with 1000 nodes in DAG, but which has 2^1000 nodes if it is fully expanded as a tree.

% ?- N=1000, test_tree(N, _Tree),
%	time((zdd use_table(simple_term_index(_Tree, I)))).
%@ ERROR: '$tbl_variant_table'/6: Not enough resources: private_table_space

Although I should learn more sophistcated use of tabling of Prolog, I feel I have to keep the imperative use of memo for the time being. Despite of my use of memo, ZDD programming seems bringing new declarative feature into Prolog. For example, though may not be appropriate appealing one, the set of paths which connect specified pair of nodes, in the end, to find a special subset of the powerset of links of the given graph. As far as I have touched documents by Minato’s group and D.Knuth on mate and frontier computation, I have been inspired by their thought which is close to dynamic programming, though my experience of logic programming is poor to say loud further on this point (even in Japanese). ZDD programming in Prolog surely is a hobby of mine, as far as it is writable for me.

I have added term_index/2 to library(pac/zdd), together with coterm/2, show_coterm/2. term_index/2 works like builtin library term_factorized/3, term_index/2 works only for well-founded ground terms, though.

% ?-  term_index(f(g(a), g(a)), I), term_index(T, I).
%@ I = 4,
%@ T = f(g(a), g(a)) .

The term f(g(a),g(a)) is internally represented by equations as that by term_factorized/3. BTW, the naming coterm is after co-algebra of the term algebra, roughly.

% ?- zdd show_coterm(f(g(a),g(a))).
%@ 4=f(3,3)
%@ 3=g(2)
%@ 2=a
%@ true.

It should be clear to recover f(g(a),g(a))) from these equations.
term_index/2 gives a unique postive integer (>2) to each term and its subterms.

term_index/2 is implemented by coterm/2. coterm/2 is a generalized cofact/2, which is most basic predicate of library(pac/zdd) such that most application predicates
(join, meet, merge, etc) are built on cofact/2.

library(pac/zdd) is a kind of hash table library. In fact,
handling ZDD as a system of families of sets is really one of applications of the elementary hash table handling (not sophisticated), though ZDD on Prolog is surely significant application of hash table, I believe.

I am wondering if the coterm/2 as a generalized cofact2 has
a significant application. I should try to find meaningful application of term_index/2, for instance, though I have no idea where to find.