Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search

We present a novel symbolic reasoning engine for SQL which can efficiently generate an input 𝐼 for 𝑛 queries 𝑃 1 , • • • , 𝑃 𝑛 , such that their outputs on 𝐼 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 𝑃 𝑖 -that is, a subset of 𝑃 𝑖 '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.