Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
summary
Polygon implements a conflict-driven under-approximation search that encodes restricted SMT models of SQL operators (joins as matrices, filters as vectors) and systematically searches a family of under-approximations until a satisfying input is found. The tool generates concrete databases to refute equivalence and to cluster queries, scales to over 30,000 benchmarks, refutes about 5,400 query pairs within one minute, and solves the 100-query disambiguation task for ≈97% of benchmarks with median times under 20s.
AI-written summary · about
chapters (11)
- 0:00Polygon and symbolic SQL reasoning
- 2:07Prior SQL reasoning approaches
- 3:31Under-approximation in Polygon
- 5:15Under-approximation with SQL examples
- 7:18Query operators for under-approximation
- 10:11SMT formulas for under-approximation
- 10:55Under-approximation families for completeness
- 12:20Conflict-driven search in under-approximation
- 13:03Evaluation and benchmarks
- 14:27Polygon performance comparison
- 15:32Q&A
related talks
15mSpeeding up Symbolic Reasoning for Relational Queries
44mIntermediate Relational Algorithm Design
16mA Compiler for Fused Relational Operations on Multisets
35mApproximating Certain and Possible Answers Beyond Sets
19mPinolo: Detecting Logical Bugs in Database Management Systems with Approximate...
04mLogic and Algorithms In Database Theory and AI
53mDirect Access for Conjunctive Queries with Negation
41mOptimizing Relational Programs I