Speeding up Symbolic Reasoning for Relational Queries
summary
Presents a space refinement algorithm that soundly shrinks the set of candidate input tables by backward-propagating provenance from a symbolic output, implemented for SQL and integrated with SMT-based solvers. Evaluated on bounded query equivalence checking, test-data generation and concolic testing, the prototype yields up to 100× speedup on real benchmarks, especially for GROUP BY and aggregation queries; it is solver-independent, does a linear backward pass, and fails to help when outputs depend on every input tuple (e.g., certain boolean-heavy queries).
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:22How people solve the problem
- 1:50The problem
- 3:35By Small Model
- 4:25True Curves
- 5:18I Problems
- 9:38Experiments
- 11:07Limitations
- 11:46Summary
related talks
20mPolygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
05mRelational Programming
41mOptimizing Relational Programs I
44mIntermediate Relational Algorithm Design
01h 05mIntroduction to Relational Algorithms
36mOptimizing Relational Programs II
16mA Compiler for Fused Relational Operations on Multisets
01h 06mAlgebraic Structures in Logic and Query Evaluation 1