Reference - Results: making BDDs from

Among the experiments we have run, those inputs relating specifically
to bounded model checking benchmarks have been obtained from the
output of the `bmc` program obtainable from Carnegie Mellon University.
That program inputs a model checking problem and a number of time
steps and outputs a propositional logic formula representing the BMC
problem in three formats: a large propositional logic formula,
three-address code representing the parse tree for that formula, and a
CNF translation of the formula. Program `bmc` internally
represents all formulas recursively as

where

We use `bmc` to generate three-address and CNF inputs directly,
instead of taking already generated CNF formulas ``off the shelf'' so
we have equivalent three-address and CNF data. Thus,
times we report for zChaff, Berkmin, and Siege may differ from
published times.

The largest propositional logic formula output by `bmc` is a
conjunction of smaller formulas, so the obvious course for SBSAT is to
read in each of those smaller formulas as a BDD. Nevertheless, for
some of the `bmc` outputs, those propositional logic formulas were
much too large even to store as BDDs. Of course, we also did not want
to use the three-address code or the CNF representation directly,
since that would negate the benefits of SMURFs which are to
retain potentially exploitable domain-specific relationships. Our
current approach is successful in spite of being amazingly simplistic.

- We read in the three-address code and recreate the large propositional formula so as not to lose domain-specific information. Starting at the bottom of this formula we start building a BDD. We use a greedy algorithm: when the BDD gets too large (10-18 variables) we insert a new variable to represent the BDD so far, include a BDD asserting that is what the new variable represents, replace the part we have translated with the new variable, and continue the process. This particular translation goes against our intention of staying in the original domain, however, this simple process still proves useful. In future research we hope to find a better algorithm.
- To break each resultant BDD down to a 10-variable maximum
(so that the SMURFs remain suitably small), we do the
following (see also Section ):
(a) Compute all projections of the BDD onto 10-variable subsets of its variable set (see Section for the meaning of projection).

(b) Simplify the 's against each other and delete resultant 's which become

`True`. Below we call the final simplified 's .Note that logically implies each ; we can think of them as ``approximations'' to , in the sense that each is false on some, but probably not all, of the truth assignments on which is false.

(c) Recall that the goal is to replace with a set of smaller BDD's. Now is logically equivalent to the conjunction of the set where

( just excludes the truth assignments where all the 's are true but is is false).If has variables, we replace with . If has variables, we replace with plus the translation of to CNF. (Typically, is satisfied in most truth assignments, so its CNF translation should be fairly short.)

Again, this procedure is simplistic. We hope in the future to find a better algorithm.