BDDs reordering

Staff
Advisers           Prof. Orna Grumberg
                          Mr. Ilan Beer

team                 Sigal Asaf
                          Yuval Emek

The project's goal
Assume the following scenario in a model-checker system (or any other system that uses BDDs):
Process A is building a BDD for a given circuit. In some stage, after part of the circuit has already been modeled, the BDD becomes to large. For that reason, process A creates  process B that has to find a better variables order for the BDD (the variables order of the BDD projects directly on its size). While process B is executing, process A continue with its work. When process B terminates we would like to modify the variables order of the BDD that process A is building, to the variables order that process B had found (that variables order should be better - the BDD's size should decrease).

For that purpose, A subroutine that reorders the BDD according to a given variables order is needed.

The goal of our project was to find such subroutine.