I am having several positive programming experiences on ZDD over the boolean ring (=GF(2)). For example, the codes gf2_sat_count count the solutions of this
a + b*c + d*e*f = 0
( I am not sure 32 is correct, which my codes just said). I am new to GF(2)
algorithm which have to take care of, e.g, x*x=1 and x+x=0, in fact, I had hard time on this (and still). In addition, I have seen that the standard order (compare/3) used in my ZDD is simply lexical total ordering which satisfies necessary condition for Groebner basis calculus. As such, I have written several basic operations, to get head term of ZDD as polynomials, polynomial residue calculus, the critical Spoly operation on GF(2) in ZDD (not lists).
I hope I could get other results on this worth to post here.
% ?- zdd((even_odd_power([1-1, 2-2, 3-3], X, Y), gf2_sat_count([Y-1], 0, C))).
%@ X = 10,
%@ Y = 9,
%@ C = 32.
%
gf2_sat_count(X, Y, Z):- shift(gf2_sat_count(X, Y, Z)).
%
gf2_sat_count([], U, U, _):-!.
gf2_sat_count([P-C|As], U, V, S):- gf2_sat_count(P, C, As, U, V, S).
%
gf2_sat_count(1, C, As, U, V, S):-!, U0 is U + C,
gf2_sat_count(As, U0, V, S).
gf2_sat_count(0, _, As, U, V, S):-!, gf2_sat_count(As, U, V, S).
gf2_sat_count(P, C, As, U, V, S):- cofact(P, t(_-J, L, R), S),
C0 is C * (2^J-1),
gf2_sat_count(R, C0, [L-C|As], U, V, S).
% ?- zdd((even_odd_power([1,2,3], X, Y), Z<<pow([1,2,3]),
% zdd_join(X, Y, Z))).
even_odd_power(X, Y, Z):- shift(even_odd_power(X, Y, Z)).
%
even_odd_power([], 1, 0, _).
even_odd_power([X|Xs], Ev, Od, S):-
even_odd_power(Xs, Ev0, Od0, S),
zdd_insert(X, Ev0, X_Od, S),
zdd_insert(X, Od0, X_Ev, S),
zdd_join(X_Od, Od0, Od, S),
zdd_join(X_Ev, Ev0, Ev, S).