EDIT: 2022/Sep/22
I have added a few lines of codes to verify that the output equations are really a solution to the given boolean equation.
It needs to check that the variables eliminated DNF is a tautology. To do so, I applied two ways, one is by propositional prover, the other is counting number of solutions of the DNF. Both were successfully checked.
BTW, on the way of this work to check solutions, I found my counting method of DNF ltr_card/3 had serious bugs. Fortunately, spending some time, I fixed the bugs in my old codes. Counting solutions to DNF is not easy as expected earlier.
Added codes to verify answer colutions and relevant queries.
% ?- ltr_zdd((E<<dnf0(x*y=a), @solve_boolean_euations(E, [x,y,z], [u,v,w], Sols), @solutions_to_sets(Sols, Sols0), @check_solutions(E, Sols, Cond), sets(Cond, Check))).
%@ E = 12,
%@ Sols = [x=33, y=23, z=26],
%@ Sols0 = [x=[[a], [-a, u, -v]], y=[[a], [-a, v]], z=[[a], [-a, w]]],
%@ Cond = 56,
%@ Check = [[a], [-a, v], [-a, -u], [-a, -v]] .
% ?- ltr_zdd((X<<dnf(a + (-a * v) + -a * -u + -a * -v), @ltr_card(X, C))).
%@ X = 17,
%@ C = 8 .
% ?- prove(a + (-a * v) + -a * -u + -a * -v).
%@ CNF has 4 clauses.
%@ VALID
%@ true .
check_solutions(Exp, Eqns, Cond, S):-
apply_subst_list(Eqns, Exp, Cond, S).
%
apply_subst_list([], E, E, _).
apply_subst_list([X=U|Eqns], E, E0, S):-
dnf_subst(X, U, E, E1, S),
dnf_subst_list(Eqns, E1, E0, S).
END of EDIT
As DNF/CNF supports of my ZDD library have made some progress, I applied it to solve boolean equations. It solves
xy = a
which seems not trivial, though I am not familiar with solving Boolean equations at all. The problem is in Tsutomu Hosoi (ISBN4-535-60118-6). The output below says x = a+au+ -au*-v and y= a + -a*v, which is a little bit redundant because
of no optimization on the solutions.
I have made the net search for “solving boolean equations”, but got nothing relevant. Is the problem nowadays out of date ? Although I would not like to go deep into solving boolean equations, but want to solve some more standard about 10 samples if any on the net. I will appreciate for relevant information.
% ?- ltr_zdd((E<<dnf0(x*y=a), @solve_boolean_euations(E, [x,y], [u,v], Sols), @sols_sets(Sols, Sols0))).
%@ E = 12,
%@ Sols = [x=47, y=28],
%@ Sols0 = [x=[[a], [a, u], [-a, u, -v]], y=[[a], [-a, v]]] .
% ?- ltr_zdd((E<<dnf0(x*y=a), @solve_boolean_euations(E, [x,y,z], [u,v,w], Sols), @sols_sets(Sols, Sols0))).
solve_boolean_euations(_, [], _, [], _):-!.
solve_boolean_euations(E, [X|Xs], [A|As], [X=Sol|Sols], S):-
solve_boolean_euations_basic(E, X, A, Sol0, E0, S),
solve_boolean_euations(E0, Xs, As, Sols, S),
dnf_subst_list(Sols, Sol0, Sol, S).
% ?- ltr_zdd((E<<dnf0(a*b+c*(-a)+b), @(solve_boolean_euations_basic(E, a, u, Sol, Cond)), psa(E), psa(Sol), psa(Cond))).
solve_boolean_euations_basic(E, X, A, Sol, Cond, S):-
dnf_subst(X, 1, E, C1, S),
dnf_subst(X, 0, E, C0, S),
ltr_join(C0, C0, Cond, S),
ltr_negate(C0, NC0, S),
ltr_insert(A, C1, AC1, S),
ltr_join(NC0, AC1, Sol, S).
% ?-ltr_zdd((X<<dnf0(-a), Z<<dnf0(b), @(dnf_subst(a, Z, X, Y)), psa(X), psa(Y))).
dnf_subst(_, _, X, X, _):- X < 2, !.
dnf_subst(V, D, X, Y, S):-
cofact(X, t(A, L, R), S),
dnf_subst(V, D, L, L0, S),
(A= -(U); U=A ),
ltr_compare(C, V, U),
( C = (<) -> Y = X
; ( C = (=) ->
( A=(-V) ->
ltr_negate(D, D0, S),
ltr_merge(D0, R, R0, S)
; A = V ->
ltr_merge(D, R, R0, S)
)
; dnf_subst(V, D, R, R1, S),
ltr_insert(A, R1, R0, S)
),
zdd_join(L0, R0, Y, S)
).
%
dnf_subst_list([], E, E, _).
dnf_subst_list([X=A|Eqs], E, F, S):-
dnf_subst(X, A, E, E0, S),
dnf_subst_list(Eqs, E0, F, S).
%
sols_sets([], [], _).
sols_sets([X = E|Sols], [X = E0|Sols0], S):-
sets(E, E0, S),
sols_sets(Sols, Sols0, S).