compute the cardinality of a substitution choice
compute the cardinality of a substitution choice
the substitution choice
the over, under and exact cardinality (if computable)
Recursively compute the cardinality of a mdd node according to a substitution choice which is card(node)=min_{s \in node.kids} (card(s.tr,choice(node))+card(s.son))
Recursively compute the cardinality of a mdd node according to a substitution choice which is card(node)=min_{s \in node.kids} (card(s.tr,choice(node))+card(s.son))
mdd node
substitution chocie
the over, under and exact cardinality (if computable)
cardinality theory which returns for a given substitution choice, the status and the propogation and conflicts.
cardinality theory which returns for a given substitution choice, the status and the propogation and conflicts. The theory try to dispatch on the trace tree a budget corresponding to the cardinality requirement. For cardinality since card(node)=min_{s \in node.kids} (card(s)+card(tr_{node \to s})), then if one path does not fulfill the requirement then the candidate does not fill the requirement. Since the substitution choice is not always complete, an over and under approximations of the budget are computed at each step.
cardinality requirement
subsitution choice
the status of the dispatch operation and the conflicts/propagations