Streaming BDD Manipulation for Large-Scale Combinatorial Problems
Shin-ichi Minato, Shinya Ishihara · 2001
We propose a new BDD manipulation method that never causes memory overflow or swap out. In our method, BDD data areaccessed 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 areconcurrently produced. Our streaming methodfeatures that (1) it gives a continuous trade-off between the memory usage and the streaming data length, (2) a valid partial result can be obtainedbeforecompleting process, and (3) easily accelerated by pipelined multiprocessing. Experimental result shows that our new methodis especially useful for the cases whereconventional BDD packages are ineffective. For example, we succeededin finding a number of solutions to a SATproblem using a commodity PC with a 64 MB memory, where the conventional method will require a 100 GB memory to compute it.