As a rule of thumb, the higher the compression the faster the algorithms.
Because higher compressions, means less many nodes to be processed by
the algorithms. For example the ltr_card/3 you posted looks a little bit slow,
what does expand_dnf/4 and card/3 do? So I guess you would be also
interested. For example your DNF give in the Lion and Unicorn example
the following result below. Thats wooping 8 million inferences!
I didn’t try yet my ZDD with Lion and Unicorn, but will post soon a ZDD
solution. Although I would like to first do Sudoku with ZDD. if a Sudoku
is determinate, this might mean we are in the green zone of ZDD.
Not yet sure, whether this reasoning applies.
Edit 15.12.2023
Seems you are going back from binate to unate, eliminating negative
literals in your representation. So that no more nodes of the form t(-X,A,B)
are around. The Prolog text zdd.pl tells me:
expand_dnf (+Vs, +X, -Y, +S) is det
With U the set of all atoms appearing in X, Y is the all maximal
complemental-free clauses C over the union of Vs and U such that C
is an extension of some clause in X.
You could have that easier, if you would compute the ZDD normal form
directly from the propositional formula. And then count the ZDD normal form.
What I am not 100% sure, is whether the result of expand_dnf/4 is a ZDD
normal form or not. It uses ltr_XXX predicates and not zdd_XXX predicates.