I am busy on revising codes for DNF/CNF converter based on ZDD. They are still enough dirty or confused for me to remember details. However I hope it will drastically be improved in a week. I will upgrade package pac with it.
IMHO, SAT solving is to get DNF as normal form of the input formula. Therefore computational complexity must be high, perhaps NP-complete, though I am not sure on this. So I am not interested in efficiency of my approach, but in conceptual clearness.
For now I can only show an example below, where psa is
to show current dnf as normal form of SAT solving.
Sorry for not able to discussing about what you might want, which
might be too difficult for me to catch up with.
% ?- sat(a=:=b), psa, sat(b=:=c),psa, sat(c=:=d), psa.
%@ zid = 8
%@ [-a,-b]
%@ [a,b]
%@ -------------------
%@ zid = 16
%@ [-a,-b,-c]
%@ [a,b,c]
%@ -------------------
%@ zid = 26
%@ [-a,-b,-c,-d]
%@ [a,b,c,d]
%@ -------------------
%@ true.