Polygon通过符号推理高效生成满足条件的SQL输入，用于验证查询等价性或消除歧义。
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
- 基于冲突驱动的欠逼近搜索，聚焦查询的部分输入输出行为
- 在3万多个基准上测试，显著优于已有方法
- 适合需要验证或对比SQL查询逻辑的开发者与研究人员
我们提出一种新的SQL符号推理引擎Polygon，能够高效生成一个输入I，使得n个查询P₁,…,Pₙ在该输入上的输出满足给定的SMT性质。该方法在验证查询等价性、消除查询歧义等场景中具有应用价值。核心思想是针对每个查询Pᵢ进行欠逼近分析——即仅考虑其部分输入输出行为。虽然该方法语义感知且轻量，但单一欠逼近可能遗漏关键行为。因此，我们进一步设计了一种覆盖所有相关程序行为的表达式族，在其中进行搜索，确保方法完备性。我们在Polygon工具中实现了上述思想，并在两个任务（查询等价性反驳与查询消歧）上对超过30,000个基准进行了评估。结果表明，Polygon显著优于所有已有技术。
原文摘要 · Abstract (English)
We present a novel symbolic reasoning engine for SQL which can efficiently generate an input $I$ for $n$ queries $P_1, \cdots, 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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。