Fast OBDD Reordering using Neural Message Passing on Hypergraph
  Ordered binary decision diagrams (OBDDs) are an efficient data structure for
representing and manipulating Boolean formulas. With respect to different
variable orders, the OBDDs' sizes may vary from linear to exponential in the
number of the Boolean variables. Finding the optimal variable order has been
proved a NP-complete problem. Many heuristics have been proposed to find a
near-optimal solution of this problem. In this paper, we propose a neural
network-based method to predict near-optimal variable orders for unknown
formulas. Viewing these formulas as hypergraphs, and lifting the message
passing neural network into 3-hypergraph (MPNN3), we are able to learn the
patterns of Boolean formula. Compared to the traditional methods, our method
can find a near-the-best solution with an extremely shorter time, even for some
hard examples.To the best of our knowledge, this is the first work on applying
neural network to OBDD reordering.
