Streaming BDD manipulation for large-scale combinatorial problems

We propose a new BDD manipulation method that never causes memory overflow or swap out. In our method, BDD data are accessed through the I/O stream ports. We can read unlimited length of BDD data streams using a limited size of the memory, and the result of BDD data streams are concurrently produced. Our streaming method features (1) a continuous trade-off between the memory usage and the streaming data length, (2) a valid partial result can be obtained before completing process, and (3) easily accelerated by pipelined multiprocessing. Experimental result shows that our new method is especially useful for the cases where conventional BDD packages are ineffective. For example, we succeeded in finding a number of solutions to a SAT problem using a commodity PC with a 64 MB memory, where the conventional method will require a 100 GB memory to compute it. BDD manipulation has been considered as an intensively memory-consuming procedure, but now we can also utilize the hard disk and network resources as well. Our method will lead a new style of BDD applications