Implicit manipulation of equivalence classes using binary decision diagrams

A novel representation called an equivalence class characterization function is defined. It can implicitly represent all equivalence classes with a compact characteristic function that will have at most n outputs. Using binary decision diagrams (BDDs) and the concept of the equivalence class characterization function, very large problem instances can be represented. For manipulating equivalence classes efficiently, a Boolean operator called a compatible projection operator is proposed. Conceptually, the compatible projection operator is used to uniquely select a single element from each equivalence class to characterize the class. In manipulating equivalence classes, the compatible projection operator is used to implicitly derive an encoding function from the equivalence relation that encodes the equivalence class information symbolically. An efficient implementation is described based on BDDs that is applied to very large problem instances