CNF/DNF are built in ZDD with almost zero cost

After a lot of small changes in my zdd library, I have checked that existing sample queries listed in source codes work as before, though it does not mean bug-free at all. Hoping that the current ZDD library including facilities on DNF/CNF has achieved enough robustness for possible applications, which I have no idea of though.

To demonstrate some of the current state of my zdd library, I wrote two codes below, and, using them build a huge DNF to count its solution. Codes of zdd_sat, zdd_sat_count, and a table for controling syntax control. I would be glad if you could suggest applications of DNS/CNS feature in ZDD.

zdd_sat/1, zdd_sat_count/1 in this query also listed below.

% ?- zdd_sat(a+b+c+d), zdd_sat_count(C).
%@ C = 15.

% ?- zdd_sat(a+b), zdd_sat(c+d),  zdd_sat_count(C).
%@ C = 9.

% ?-zdd_sat(a->b), zdd_sat(b->c), zdd_sat(c->d), zdd_sat(d->a), zdd_sat_count(C).
%@ C = 2.

% ?- zdd_sat(X=(a=b)), zdd_sat(Y=(b+c)), zdd_sat(X=Y), zdd_sat_count(C).
%@ X = C,
%@ Y = F,
%@ C = 4.

% ?- zdd_sat(X=(a=b)), zdd_sat(Y=(b+c)), zdd_sat(X=Y), zdd_sat(X = (-Y)).
%@ false.

% ?- zdd_sat(*[p(1),p(2)]), zdd_sat_count(C).
%@ C = 1.

% ?- zdd_sat(+[p(1),p(2)]), zdd_sat_count(C).
%@ C = 3.

% ?- N=10, findall(p(I, J), (between(0, N, I), between(0, N, J)), L), zdd_sat(+L), zdd_sat_count(C).
%@ N = 10,

%@ L = [p(0, 0), p(0, 1), p(0, 2), p(0, 3), p(0, 4), p(0, 5), p(0, 6), p(0, 7), p(..., ...)|...],
%@ C = 2658455991569831745807614120560689151.

% ?- N=10, findall(p(I, J), (between(0, N, I), between(0, N, J)), L), zdd_sat(*L), zdd_sat_count(C).
%@ N = 10,
%@ L = [p(0, 0), p(0, 1), p(0, 2), p(0, 3), p(0, 4), p(0, 5), p(0, 6), p(0, 7), p(..., ...)|...],
%@ C = 1.
	(	nb_current(sat_state, S),  S \== [] -> true
		set_compare(ltr_compare, S),
		b_setval(sat_state, S)
	b_getval(sat_state, S),
	get_key(root, Root, S),
	dnf(X, Y, S),
	ltr_merge(Y, Root, Root0, S),
	set_key(root, Root0, S),
	Root0 \== 0.
zdd_sat_count(C):- b_getval(sat_state, S),
	get_key(root, X, S),
	get_key(atom_index, N, S),
	N0 is N - 2,
	ltr_card(N0, X, C, S).

Surfice syntax of boolean expression is controled by the following table, role of which should be clear.

% Variaous logical connectives.
boole_op(0, [], [true], 1).
boole_op(0, [], [false], 0).
boole_op(1, [X], [-, ~, \+, not], -X).
boole_op(2, [X, Y], [and, &, /\, ',', *], X*Y).
boole_op(2, [X, Y], [or, '|', \/, ';', +], X+Y).
boole_op(2, [X, Y], [->, imply], -(X)+Y).
boole_op(2, [X, Y], [<-], X + -Y).
boole_op(2, [X, Y], [==, =,  =:=, equiv, ~, <->, <=>], -X* -Y + X*Y).
boole_op(2, [X, Y], [=\=, \=], -X*Y + X* -Y).
boole_op(2, [X, Y], [exor, #], X* -Y + -X *Y).
boole_op(2, [X, Y], [nand], -(X*Y)).

End of EDIT.

The codes listed below is a simple but powerful prover on proposinal logic in CNF (Conjunctive Normal Form). I remember I posted the same codes in the last year, but I doubted its correctness at that time, partially because it was written in a hurry as a tentative debugging case of my ZDD library. However still I can’t find any logical bug on that simplest codes. On the contrary the algorithm behind the codes now seems clearly correct based on the induction on the number of literals. As operations in the codes are all simply those of zdd, in other words it is written within familiar basics of zdd. There seems no room for logical bugs to stay in such tight space.

Thus, CNF is so basic, but needless to say, in order to get CNF, given structural information on logical equivalence and implicational are smashed into ‘and’, ‘or’, ‘not’. That’s too bad. But anyway CNF is built into ZDD with almost zero cost. In addition, DNF (disjunctive normal form) is built into ZDD at the same time, which is useful for fast counting solutions. I would be happy to share experience with others who are interested in ZDD.

resolve(X):- shift(resolve(X)).

resolve(X, S):- zdd_has_1(X, S), !.     % The empty clause found.
resolve(X, S):- X > 1,
	cofact(X, t(A, L, R), S),
	(	A = -(_) -> resolve(L, S)		% Negative pure literal rule.
	;	(	cofact(L, t(B, U, V), S),	% Pure literal rule.
			(	B = -(A)
			->  ltr_merge(V, R, M, S),  % Resolution + Tautology rule.
				ltr_join(U, M, W, S),
				resolve(W, S)			% Updated set of clauses.
			;	resolve(L, S)			% Posituve pure literal rule.

A sample query to show some power of the prover resove. It solves for a special CNF consisting of N clauses where N= 633825300114114700748351602688. The sample CNF is the conjunction of all possible clauses of complementary-pair-free literals. For example, [[2,3],[-2,3], [2, -3], [-2, -3]] (0, 1 are reserved for ZDD).

% ?- N=100, numlist(2, N, Ns), time(zdd((shift(sample_cnf(Ns, X)), card(X, C), resolve(X)))).
%@ % 2,532,002 inferences, 0.609 CPU in 1.005 seconds (61% CPU, 4154910 Lips)
%@ N = 100,
%@ Ns = [2, 3, 4, 5, 6, 7, 8, 9, 10|...],
%@ X = 298,
%@ C = 633825300114114700748351602688.
sample_cnf([], 1, _).
sample_cnf([J|Js], X, S):- sample_cnf(Js, Y, S),
	ltr_insert(J, Y, Z, S),
	ltr_insert(-J, Y, U, S),
	ltr_join(Z, U, X, S).

My educated guess is maybe your ZDD (Zero-suppressed decision diagram - Wikipedia) has much common with William Bricken’s iconic math / boundary logic???!!
Please check the page 32 of

Bricken never mentions ZDD in the pdf, I have studied this pdf a lot.

I am afraid it will take some time for me to read recommended two articles from iconicmath. I read a copy of a book in Japanese on Spencer-Brown’s thought about three decades ago, bu it was far high beyond my reach. Anyway I will find time to read the articles hoping to reply something. Thanks.

I have failed to find the common you suggest. I think it is your own discovery if they exist. Of course, I have in mind that might be related to "iconic math; type, token, classifications, informorphism, constraints, … which are described in Barwise & Seligman’s book, which I mentioned somewhere including a pointer to a relevant toy cgi page of mine. I have a plan to develop it further with exploiting the existing power of ZDD technology. This is all what I could tell you, though I should not have done so because of its poor state of development.

This question is an important question, though I have no idea to answer for now. Some works on this should exist. I only guess a possible answer is a Gibsonian explanation(The echological approach to the visual perception) and related to J.L Austine (How to Do Things with Words" (1962)) . I am afraid that this is not an answer to the question at all.

About 20 years ago, there were already projects on sitated learning, situated robotics, visual inference, and so on which were close to Barwise/Seligman, which had been in turn influenced by Gibson and Austin (Situation semantics, Barwise & Perry see wikipedia). I am not sure this is appropriate response, but anyway it seems that you have enough knowledge on short term memory not to ask me.

Yes. But with restriction; the clauses must be ground. However, there may be a way to loosen this restriction by introducing variant identity of clauses. I am not sure for now how much does this weaken the merit of ZDD. I suspect also true experts on ZDD know about this fundamental question. I am a disguised expert, sorry.

That’s great of CLP(B) ! ZDD does not have it. If ZDD uses attributes variables (unify-hook) as some ZDD intial version it might be easy for ZDD to have such reification.

I was serious about prolog unification X=Y between boolean variables. An easy way might be to think X= Y as logical equivalence (X->Y) /\ (Y->X). But I wanted X=Y as a meta operation such like prolog internal deref operation. Although it was simple and easy to write such operation, but it seemed exceptionally expensive operation compared with other efficient basic operations. For now I am busy to debug a new codes on the notorious path counting problem of the rect(W,H).
I am happy with reification being monopoly of CLP(B).

No. There is nothing like a constraint solver inside the current ZDD of mine in any sense, but just a set of set-theoretical well-known basic operations on families of sets. However a simple constraint on cardinality, for example, might be useful, though I have no idea what kind of constraint is really useful.

DNF, a library on ZDD, converts a given proposition “(a;b),(c;d)” to a DNF [[a, c], [a, d], [b, c], [b, d]] in the standard form.

% ?- zdd(( dnf(((a;b),(c;d)), X), sets(X, L), extern(L, E), ltr_card(X, C))).
%@ X = 13,
%@ L = [[2, 4], [2, 5], [3, 4], [3, 5]],
%@ E = [[a, c], [a, d], [b, c], [b, d]],
%@ C = 9 .

There is nothing to do with boolean constraint, I thought. However, as you pointed this conversion operation surely uses properties of the boolean algebra, which might mean that
this conversion is a constraint solver, though I see nothing clever worth in the conversion to be called so.

Once I wrote a code counting solutions of the N-queen problem in ZDD. I lost the codes. If your challenge is related to this counting problem, I would like to try it again. However, even if it is so, I am afraid I could not find time until the current debugging work will be done.

I made a poor seach by git log | grep queen.
According to the log below. There seems nothing interesting in my codes on counting solutions of n-queen problem, which is a little bit strange. I have to check the codes, not now but in the future.

% ?- time(zdd(n_queens(13, C))).  % [2018/11/01]
%@ % 288,612,429 inferences, 36.548 CPU
% ?- time(zdd(n_queens(14, C))).	% [2018/10/25]
%@ % 1,743,638,761 inferences, 256.849 CPU
%@ C = 365596 .
% ?- time(zdd(n_queens(14, C))).	% [2020/10/16]
%@ % 2,003,469,945 inferences, 221.555 CPU in 223.231 seconds (99% CPU, 9042752 Lips)
%@ C = 365596 .
% ?- time(zdd_misc:usual_n_queens(13, C)).
% ?- time(zdd_misc:usual_n_queens(14, C)).
%@ % 1,360,772,993 inferences, 175.021 CPU in 175.629 seconds (100% CPU, 7774894 Lips)
%@ C = 365596 .

As I said, it is difficult to find time to write codes in ZDD for the proposed problem. I am busy for digesting
Knuth’s Simpath Algorithm , though I haven’t read the paper yet. Yesterday night, I found an initial experimental version works. It works in so beautiful way, I feel I might have got something about simpath method. I have to thank to tutorials on the net by Minto’s group on ZDD. I made sometime cherry-picking from them. Now my interest is performance of ZDD library of mine, on which I feel poor as I said on path counting in rectangular grid graph rect(w, h) compared with published performance by Minato’s group.

1 Like

(Nothing of Importance here)

藤井聡太(Fujii Souta) is a young super hero in Japanese professional Chess(将棋). I heard that when young (still young) he polished his genious skill by using computer software.
one of the strongest
big hint to Ponanza
It seems that human professional players and computer software coexist also in a sense of business, which is a usual and traditional scenes in the history of Japan. I like it.

According to Apple bundled dictionary, threatmate is 必死 (inevitability), stalement is 千日手 (a thousand days long turns, i.e. deadlock).

I remember that once I tried to build and-or tree, which is not in ZDD, and got nothing (as almost always). I don’t remember the motivation of the trial. I will check around the and-or trees in ZDD when I will have time. Thanks.

I might be hearing a music of duet of findall/3 and zdd written in SWI-Prolog codes. The findall/3 is used in preprocessing to give two linear orders on grids of the rectangle. One is the standard orthogonal, the other is skewed coordinates. Note that the preprocessing is neglegible compared with the whole process. Despite of W. Jan’s warning on findall use, I think it is useful to make my codes less obscure, which is important to me. I posted the standard order already works. This time I tested whether the same zdd logic works for the skewed ordering. The result is fine as partially listed below.

I forgot time/1 for the query. For the time being, details is black-box. Now it is time to think how to open the box to interested hopefully friendly readers, though no idea yet.

% ?- call_with_time_limit(36000, count_rect_path(rect(11,11), C, _)).
%@ p(22,11)
%@ p(21,11)
%@ p(21,10)

( as vertical progressive bar )

%@ p(2,0)
%@ p(1,1)
%@ p(1,0)
%@ p(0,0)
%@ C = 182413291514248049241470885236.


		*     Switches    *

% rect_nodes(X, Y):- rect_nodes_orth(X, Y).
% active_node(X, Y):- active_node_orth(X, Y).

% For SKEW.
rect_nodes(X, Y):- rect_nodes_skew(X, Y).
active_node(X, Y):- active_node_skew(X, Y).
rect_nodes_orth(R, PES):-
	findall(P-E, (in_rect(P, R), node_ends(P, E, R)), PES).
rect_nodes_skew(R, PES_skew):- rect_nodes_orth(R, PES_orth),
	  convert_orth_skew(PES_orth, PES_skew).

(top main).

count_rect_path(Rect, C, Opts):-
	memberchk(state(S), Opts),
	memberchk(out(X), Opts),
	set_compare(link_compare, S),
	set_key(rect, Rect, S),
	rect_nodes(Rect, A),
	sort(A, A1),
	reverse(A1, B),
	B =[Max-_|_],
	set_key(max, Max, S),
	node_one_by_one(B, 1, X, S),
	card(X, C, S).

(Nothing of Importance here)

If I understand correctly, it is not related to DNF/CNF but directly to ZDD:
Enumarate all TRUE situations, say T. Then for a given ( partial) situation s one can ask T whether s is in T or extendible to some situation in T. Also similarly negative check. I am not sure on details. It sounds as so typical and interesting problem for ZDD that I suspect an answer is already prepared somewhere.

If your problem is to do with finding all closed paths in a graph, then codes which I’m currently developing might be directly usable with minor changes, which would be conincidence. Not sure, and I am really afraid I am going to add a case of nothing important. I should be careful enough to write only after an experiment when I would have time, provided that it is related to your problem.

Now I got fire under my nails. ZDD could be used to not only
map a situation to TRUE or FALSE, maybe it could be used to
map a situation to an evaluation? (*)

Stockfish - Strong open source chess engine
(Currently in Legal War with ChessBase Fat Fritz 2)

Actually an AlphaGo inspired machine learnt evaluation function,
would maybe already pay half the rent of a chess game?
Simple evaluation functions only measure the material on

the chess board, and not some geometry.

Edit 02.08.2022:
(*) How can a boolean formula be a map? Well if we take some input
propositional variables x1,…,xn and view the rest of the propositional
variables y1,…,ym in the formula as output, we get a relation. This

relation can be functional. For an evaluation we need some bits
in y1,…,ym to compute a value. My expectation is that ZDD is an
alternative tabling method, and you don’t need any intelligent

algorithms to use it. Just populate ZDD with some brute force
algorithm and you get a compressed map, ready to use.