Conditional doesn't backtrack for solution

No. It can’t. It (mine) only translates a proposition to
its logically equivalent DNF whose conjunction has not a complementary-pair, and in addition counts the number of solutions (assignments) if required. However ZDD for finite domain constraint calculus sounds somehow possible, though specification of the goal of the problem is unclear for me, who is not familiar with it.