CIF data-based synthesis NodeOrderer/ReverseOrderer sorts partitions in wrong order
Partition sorting
NodeOrderer
currently does:
// Sort the partitions on descending size. This puts unconnected nodes at the end of the computed order.
Collections.sort(partitions, Comparator.comparingInt((List<Node> p) -> p.size()).reversed());
In the paper that introduces DCSH, Algorithm 1, unconnected nodes are put at the front of the computed order:
Set R equal to R appended to E
'R' is the computed order, and 'E' the unconnected nodes. The sentence is a bit confusingly written. It is 'R := E + R', rather than 'R := R + E' as I originally read it. This is thus not implemented as in the paper. Changing this may improve synthesis performance, as more relevant variables should be at the end of the variable order, as then they are closer to the bottom of the BDD.
Note that the algorithm in the paper only supports unconnected variables and a single partition with all other variables. Our implementation allows arbitrary partitions.
Since variable ordering heuristics are heuristics, I don't necessarily consider it a bug. I labeled this issue an enhancement, as it may improve performance.
Reversing the order
In DCSH, we already also use the reverse variable orders as well, as in the algorithm in the paper. However, the MSc report indicates:
When reversing the order we make sure that if any unconnected nodes in the adjacency graph appear, they are always placed at the front of the ordering, as this reduces the WES.
When we reverse the order, we reverse it completely, ignoring partitions. Thus, the unconnected nodes don't remain at the front (or rather, at the back, where they are now). Taking into account partitions when reversing the variable order could improve performance as well.
Note that if we have partitions with variables [[1], [2], [3], [4, 5, 6]] and we flatten this as we do now, and then reverse it, we get [6, 5, 4, 3, 2, 1]. If we keep the partitions in order, and only reverse within partitions, we get [1, 2, 3, 6, 5, 4]. Other variants could potentially also be possible, I suppose.