Reference - Preprocessing

Top-level Boolean functions are expressed internally as Binary Decision Diagrams or BDDs. This allows the use of a number of new and old BDD operations to be used to, in some sense, reduce the complexity of an input problem before applying search. A simple description of BDDs is given and that is followed by a description of the preprocessing operations made available for input problem reduction.

- Binary Decision Diagrams (BDDs)
- Pattern Matching: CNF
- Generalized Cofactor (GCF)
- Branch Pruning
- Strengthening
- Inferences
- Existential quantification
- Clustering + Existential Quantification
- Clustering + Existential Quantification + Safe
- Dependent variable clustering
- Rewind
- Splitter
- Universe

John Franco 2011-09-15