next up previous contents
Next: Universe Up: Reference - Preprocessing Previous: Rewind   Contents


Splitter

The splitter is intended to replace large BDDs with sets of small BDDs. This is required in two circumstances. First, one of the objectives of preprocessing is to reveal inferences that may be used to reduce the size of the input before search is applied. This is done by applying various BDD operations which may result in some BDDs being fairly large. But SMURFs must be created from small BDDs. So the large BDDs must be split into small ones which are turned into SMURFs. This is accomplished by the splitter. Second, when using the three-address code available from the output of the bmc tool (see Section [*]), large BDDs result and the splitter is used to create smaller ones from the larger ones so reasonable sized SMURFs can be created from them.

The splitter can be turned on by the user with the -Sp 1 command line option. The maximum number of variables to split on is controlled from the command line using the -do-split-max-vars <number> switch (Page [*]). The number of variables to split on is 10 by default.

The splitter will first try to break up all big BDDs by selecting a big BDD $f$ and projecting $f$ onto all 10-variable subsets of it's variable set. We could think of each projection $f_i$ as a weak approximation to $f$. We collect these projections together and use branch pruning to simplify the collection. To ``project'' an $f$ onto a set of variables means to quantify out all variables not in that set (see Section [*] for details).

Finally, see how close we've come to $f$: conjoin all these approximations $f_i$ together, yielding $f^\prime$, and replace $f$ with $and(f, not(f^\prime))$. If some BDDs still exist with more than 10 variables then the splitter will break all remaining big BDDs into clauses.


next up previous contents
Next: Universe Up: Reference - Preprocessing Previous: Rewind   Contents
John Franco 2011-09-15