Rewrite systems [6, 10, 12] have been widely employing equality saturation [9], which is an optimisation methodology that uses a saturated e-graph to represent all possible sequences of rewrite simultaneously, and then extracts the optimal one. As such, optimal results can be achieved by avoiding the phase-ordering problem. However, we observe that when the e-graph is not saturated, it cannot represent all possible rewrite opportunities and therefore the phase-ordering problem is re-introduced during the construction phase of the e-graph. To address this problem, we propose MCTS-GEB, a domain-general rewrite system that applies reinforcement learning (RL) to e-graph construction. At its core, MCTS-GEB uses a Monte Carlo Tree Search (MCTS) [3] to efficiently plan for the optimal e-graph construction, and therefore it can effectively eliminate the phase-ordering problem at the construction phase and achieve better performance within a reasonable time. Evaluation in two different domains shows MCTS-GEB can outperform the state-of-the-art rewrite systems by up to 49x, while the optimisation can generally take less than an hour, indicating MCTS-GEB is a promising building block for the future generation of rewrite systems.

翻译：重写系统[6, 10, 12]已广泛采用等式饱和[9]技术，这是一种优化方法，通过使用饱和的e-graph同时表示所有可能的重写序列，并提取最优结果。因此，通过避免阶段排序问题可实现最优结果。然而，我们观察到当e-graph未饱和时，它无法表示所有可能的重写机会，因此在e-graph构建阶段会重新引入阶段排序问题。为应对此问题，我们提出MCTS-GEB——一种将强化学习（RL）应用于e-graph构建的通用域重写系统。其核心思想是使用蒙特卡洛树搜索（MCTS）[3]高效规划最优的e-graph构建，从而有效消除构建阶段的阶段排序问题，并在合理时间内取得更优性能。在两个不同领域的评估表明，MCTS-GEB可将性能提升至现有最先进重写系统的49倍，且优化过程通常可在1小时内完成，这表明MCTS-GEB是未来生成重写系统的一种极具前景的基础组件。