一句话：提出 Polygon，用冲突驱动欠近似搜索为 SQL 查询生成满足 SMT 属性的输入，以反驳等价性或消歧查询。
论文面向 SQL 查询的符号推理问题：给定多个查询 P1,...,Pn，需高效生成一个数据库实例 I，使其输出满足用 SMT 编码的属性，以支持 SQL 等价性反驳和查询消歧等任务。方法上，Polygon 首先对每个查询构造欠近似，即其输入-输出行为的一个子集，使推理语义感知且轻量；但固定欠近似不完备，会遗漏关注行为。为此，作者在一族可表达且能共同覆盖所有关注程序行为的欠近似上进行冲突驱动搜索，从而恢复完备性。工具在超过 30,000 个基准上评估两个任务，显示显著优于先前技术。
We present a novel symbolic reasoning engine for SQL which can efficiently generate an input I for n queries P 1 , ⋯, P n , such that their outputs on I satisfy a given property (expressed in SMT). This is useful in different contexts, such as disproving equivalence of two SQL queries and disambiguating a set of queries. Our first idea is to reason about an under-approximation of each P i –that is, a subset of P i ’s input-output behaviors. While it makes our approach both semantics-aware and lightweight, this idea alone is incomplete (as a fixed under-approximation might miss some behaviors of interest). Therefore, our second idea is to perform search over an expressive family of under-approximations (which collectively cover all program behaviors of interest), thereby making our approach complete. We have implemented these ideas in a tool, Polygon , and evaluated it on over 30,000 benchmarks across two tasks (namely, SQL equivalence refutation and query disambiguation). Our evaluation results show that Polygon significantly outperforms all prior techniques.
@article{paperbot3094,
title = {Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search},
author = {Pinhan Zhao and Yuepeng Wang and Xinyu Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729303}
}