TLDR: e-boost is a novel framework designed to accelerate e-graph extraction, an NP-hard combinatorial optimization problem critical in logic synthesis and formal verification. It addresses the trade-off between speed and optimality by combining parallelized heuristic extraction for rapid search space pruning, adaptive threshold-based reduction of candidate solutions, and warm-started exact solving using Integer Linear Programming. This hybrid approach delivers significant runtime speedups (up to 558x over ILP, 138x over SmoothE) and improved solution quality (19.04% over SmoothE), leading to practical benefits like 7.6% and 8.1% area reductions in logic synthesis tasks.
E-graphs are powerful data structures that have gained significant attention in fields like logic synthesis and formal verification. They are used to represent and optimize complex expressions by exploring vast spaces of equivalent forms. A crucial step in this process is ‘e-graph extraction,’ which involves selecting the most optimal expression from potentially countless equivalent options within the e-graph. However, this extraction is a notoriously difficult problem, classified as NP-hard, meaning it becomes computationally very expensive as the problem size grows.
Traditional approaches to e-graph extraction face a dilemma. Heuristic methods are fast but often sacrifice the quality of the solution, leading to suboptimal results. On the other hand, exact methods, which guarantee optimal solutions, are too slow and computationally demanding for practical, real-world problems. This trade-off has been a major bottleneck, limiting the widespread adoption of e-graph-based optimization techniques.
Introducing e-boost: Bridging the Gap
A new framework called e-boost has been developed to overcome this fundamental challenge. Created by researchers Jiaqi Yin, Zhan Song, Chen Chen, Yaohui Cai, Zhiru Zhang, and Cunxi Yu from the University of Maryland, College Park, and Cornell University, e-boost aims to provide both speed and high-quality solutions for e-graph extraction. The core idea is to combine the best aspects of fast heuristics and precise exact solvers.
e-boost achieves this through three key innovations:
1. Parallelized Heuristic Extraction
The first innovation focuses on speeding up the initial phase of extraction. Traditional heuristic algorithms often process e-graph nodes one by one, which can be slow. e-boost introduces a parallelized heuristic algorithm that can process multiple e-nodes simultaneously. This is possible because the calculations for different parts of the e-graph have ‘weak data dependence,’ meaning they don’t strictly rely on a specific processing order. By leveraging multi-threading, e-boost significantly reduces the time needed for the heuristic phase without compromising the quality of the initial solution.
2. Adaptive Search Space Pruning
Even with faster heuristics, the search space for optimal solutions can still be enormous. e-boost addresses this by employing an ‘adaptive search space pruning’ technique. After the initial heuristic calculation, it identifies the minimum cost for each group of equivalent expressions (e-class). It then uses a flexible threshold to filter out less promising candidates, retaining only those e-nodes whose costs are close to the minimum. This dramatically shrinks the problem size, making it much more manageable for the subsequent exact solver, while still preserving near-optimal solutions.
3. Initialized Exact Solving
With the search space significantly reduced, e-boost then applies an exact solver. It formulates the pruned problem as an Integer Linear Program (ILP), a type of mathematical optimization problem. Crucially, e-boost uses the high-quality solution found by its heuristic phase as a ‘warm-start’ for the ILP solver. This means the solver doesn’t start from scratch but is guided towards a good solution much faster, focusing its computational power on the most relevant parts of the problem.
Also Read:
- Piecewise-Affine Regularization: A Framework for Quantized Machine Learning Models
- New Insights into Counting Models in Logic: The Impact of Multiple Axioms
Impressive Performance and Real-World Impact
The results of e-boost are compelling. Across a wide range of benchmarks in formal verification and logic synthesis, e-boost demonstrated a remarkable 558 times runtime speedup compared to traditional exact approaches (ILP). It also showed a 19.04% performance improvement over SmoothE, a state-of-the-art differentiable extraction framework. For the largest and most complex benchmarks, where other methods often failed to provide any valid solution within time limits, e-boost consistently delivered.
Beyond theoretical benchmarks, e-boost also proved its practical value in realistic logic synthesis tasks. When integrated into an e-graph based logic synthesis tool, it produced significant area improvements in circuit designs—7.6% and 8.1% reductions compared to conventional synthesis tools, depending on the technology mapping libraries used. This demonstrates that e-boost’s improved extraction directly translates into more compact and efficient hardware designs.
e-boost is available as an open-source project, allowing others to benefit from and contribute to this innovative framework. You can find more details in the research paper: e-boost: Boosted E-Graph Extraction with Adaptive Heuristics and Exact Solving.
