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
cardinality theory trait based on MDD analysis
(Since version KCR analyser 1.0) old version of safety theory not using clause minimisation