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

arXiv: https://arxiv.org/abs/2504.06542 · HTML: https://mlsanity.com/paper/2504.06542/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Knowledge- and tool-augmented reasoning, one of 17 directions in LLM reasoning.
- Builds on 13 of its 69 references that are in the map.
- First posted on arXiv 9 Apr 2025.

## Placed in

- LLM reasoning / [Knowledge- and tool-augmented reasoning](https://mlsanity.com/lr/knowledge-and-tool-augmented-reasoning/)

## Builds on (most cited first, 13 of 13)

- [A Survey of Symbolic Execution Techniques](https://mlsanity.com/paper/1610.00502/) (2016)
- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries](https://mlsanity.com/paper/1802.02229/) (2018)
- [HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics](https://mlsanity.com/paper/1607.04822/) (2016)
- [VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints](https://mlsanity.com/paper/2403.03193/) (2024)
- [Data Generation for Testing and Grading SQL Queries](https://mlsanity.com/paper/1411.6704/) (2014)
- [Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)](https://mlsanity.com/paper/2301.10037/) (2023)
- [CUBES: A Parallel Synthesizer for SQL Using Examples](https://mlsanity.com/paper/2203.04995/) (2022)
- [Beginner's Luck: A Language for Property-Based Generators](https://mlsanity.com/paper/1607.05443/) (2016)
- [A True Positives Theorem for a Static Race Detector - Extended Version](https://mlsanity.com/paper/1811.03503/) (2018)
- [Data Migration using Datalog Program Synthesis](https://mlsanity.com/paper/2003.01331/) (2020)
- [An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More](https://mlsanity.com/paper/2003.04791/) (2020)
- [Polymorphic Coverage Types](https://mlsanity.com/paper/2304.03393/) (2023)

## Abstract (arXiv)

We present a novel symbolic reasoning engine for SQL which can efficiently generate an input I for n queries P1, cdots, Pn, 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 Pi -- that is, a subset of Pi'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.