EDIT:2022/Jul/20
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.
zdd_sat(X):-
( 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.
)
)
).
EDIT.
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).