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}
}