Sifting Algorithm #535

SSoelvsten · 2023-08-30T17:21:37Z

The most successful approach for variable reordering in conventional BDD packages is the sifting algorithm. This algorithm depends on the ability to efficiently swap two neighbouring variables.

Preliminary Issues

In Rename label to level #407 , we begin differentiating between a node's level and its label.
In Levelized Files #154 , we split the node-based representation to be a single file per level.

Tasks

Variable Swapping

Implement the variable swapping operation: given two variables x and y that are adjacent and x < y, swap their levels such that y < x.

Label or Level?

The basic idea behind the swapping algorithm is to move the nodes around in a way such that in-going edges can be preserved. To do this, we have to keep quite a few things in mind:

Any node with variable y should be kept as-is since its parents z < x, y may reference it.
The nodes in x that are independent of y should be kept as-is for parents z < x
Nodes with variable x that is dependent on y needs to be replaced with a new node with variable y to one or two new nodes with variable x.

Note that there is a conflict above. Both (1) and (2) are trivial if the parents only know the label and not the level of its children. Yet, (3) wants the parents to be independent of the label and not the level. Here are some ideas for (slightly unsatisfactory) implementations of variable swapping:

In [Ranjan97, Fig. 3], they circumvent the level vs. label issue by inserting forward nodes, i.e. adding redundant nodes to be cleaned up later. At first glance, I am not confident this would work for Adiar since it introduces backward edges in the DAG. How can this be cleaned up efficiently?
One other possible idea is to slightly restrict the way we can swap variables. Notice, we can propagate the node renaming due to (1) and (2) or due to (3) to their parents with a single priority queue (and the transposed graph). Hence, we might allow one to use multiple variable swaps on-top of each-other but that the levels must be monotonically decreasing. Alternatively, we could use a map with all the swaps done to the levels below.

Hopefully, we can come up with an approach that can cover (1), (2), and (3) above without having to update any parents or break the graph in an inconvenient way.

Node Preservation

Both the file for x and y need to keep (some of?) the original nodes.

To not have to update any parents, these nodes need to preserve their level id too. Hence, each swapping operation must include a set of candidate new nodes that may or may not just be merged with other nodes at said level. To do so, we need to sort the nodes (similar to the Reduce algorithm).
In [Rudell93] it is pointed out, that a y node with only x node parents can be garbage collected as part of the swapping operation. Yet, to know whether this is the case, we need to somehow have the (number of?) parents available. That is, we either need the transposed graph or a reference count on each node.