Fast OBDD Reordering using Neural Message Passing on Hypergraph

TL;DR

This paper introduces a neural message passing approach on hypergraphs to predict near-optimal variable orders for OBDDs, significantly reducing computation time and handling complex formulas more efficiently.

Contribution

It presents the first neural network-based method for OBDD reordering, leveraging hypergraph message passing to improve efficiency and solution quality.

Findings

Achieves near-optimal variable order predictions with shorter computation times.

Outperforms traditional heuristics on complex Boolean formulas.

First application of neural networks to OBDD reordering.

Abstract

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.