next up previous contents
Next: Binary Decision Diagrams (BDDs) Up: SBSAT User Manual and Previous: Boolean functions   Contents

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.


John Franco 2011-09-15