一句话:提出基于关系连接与查询计划的 e-matching,保证最坏情况最优运行时间,并在 egg 中大幅加速。
e-matching 是 e-graph 上等式饱和等技术的核心操作,传统回溯方法通常自顶向下搜索,难以充分利用模式结构,且缺乏数据复杂度分析。本文将其重新表述为关系连接,借鉴数据库查询执行技术,按照优化查询计划在 e-graph 中搜索,从而保证最坏情况最优运行时间。作者还给出首个 e-matching 数据复杂度结果,将运行时间限制为 e-graph 大小与输出大小的函数。在 state-of-the-art 的 egg e-graph 框架中原型实现并评估,相比传统基线更易实现,实际中快几个数量级。
We present a new approach to e-matching based on relational join; in particular, we apply recent database query execution techniques to guarantee worst-case optimal run time. Compared to the conventional backtracking approach that always searches the e-graph "top down", our new relational e-matching approach can better exploit pattern structure by searching the e-graph according to an optimized query plan. We also establish the first data complexity result for e-matching, bounding run time as a function of the e-graph size and output size. We prototyped and evaluated our technique in the state-of-the-art egg e-graph framework. Compared to a conventional baseline, relational e-matching is simpler to implement and orders of magnitude faster in practice.
@article{paperbot1592,
title = {Relational e-matching},
author = {Yihong Zhang and Yisu Remy Wang and Max Willsey and Zachary Tatlock},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498696}
}