Back to papers
Automated Verification of Query Equivalence Using Satisfiability Modulo Theories
Summary: Maps SQL to first-order logic and uses SMT to verify equivalence, addressing complex predicates and three-valued logic beyond algebraic approaches. EQUITAS delivers ~27x faster verification and detects 11% redundancy in 17,461 real queries; deployed on Alibaba MaxCompute.
(summarized by gpt-5-nano on Feb 09 2026)
- Paper ID
- 11824
- Venue
- VLDB
- Year
- 2019
- Pagerank
- 6.6439695e-05
- Overall Rank
- 3,903 | 72.88%
- DOI
-
10.14778/3342263.3342267
Incoming Non-self Citations Over Time
Incoming Citations (Sorted by Pagerank)
Showing 15 of 15 citing papers.
| Rank |
Citing Paper |
Year |
Venue |
Pagerank |
| 2,595 |
WeTune: Automatic Discovery and Verification of Query Rewrite Rules |
2022 |
SIGMOD |
8.4725961e-05 |
| 3,610 |
EVA: A Symbolic Approach to Accelerating Exploratory Video Analytics with Materialized Views |
2022 |
SIGMOD |
6.919859e-05 |
| 3,623 |
Cost Models for Big Data Query Processing: Learning, Retrofitting, and Our Findings |
2020 |
SIGMOD |
6.9017341e-05 |
| 4,385 |
Proving Query Equivalence Using Linear Integer Arithmetic |
2023 |
SIGMOD |
6.2247394e-05 |
| 4,661 |
Efficient Answering of Historical What-if Queries |
2022 |
SIGMOD |
6.0069281e-05 |
| 5,245 |
QED: A Powerful Query Equivalence Decider for SQL |
2024 |
VLDB |
5.6017846e-05 |
| 7,137 |
Automated Validating and Fixing of Text-to-SQL Translation with Execution Consistency |
2025 |
SIGMOD |
4.8165495e-05 |
| 7,278 |
Sia: Optimizing Queries using Learned Predicates |
2021 |
SIGMOD |
4.7720613e-05 |
| 8,339 |
SlabCity: Whole-Query Optimization using Program Synthesis |
2023 |
VLDB |
4.5383933e-05 |
| 8,625 |
Predicate Pushdown for Data Science Pipelines |
2023 |
SIGMOD |
4.4784651e-05 |
| 8,780 |
GEqO: ML-Accelerated Semantic Equivalence Detection |
2023 |
SIGMOD |
4.4485568e-05 |
| 9,623 |
Qr-Hint: Actionable Hints Towards Correcting Wrong SQL Queries |
2024 |
SIGMOD |
4.3120302e-05 |
| 10,577 |
QOVIS: Understanding and Diagnosing Query Optimizer via a Visualization-assisted Approach |
2025 |
VLDB |
4.1905499e-05 |
| 10,768 |
ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation |
2025 |
VLDB |
4.1905499e-05 |
| 11,222 |
Lightweight Materialization for Fast Dashboards Over Joins |
2023 |
SIGMOD |
4.1905499e-05 |
Outgoing Citations (Sorted by Pagerank)
Showing 13 of 13 cited papers.
Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.
| Rank |
Cited Paper |
Year |
Venue |
Pagerank |
| 335 |
Optimization of Real Conjunctive Queries |
1993 |
PODS |
0.00027012705 |
| 401 |
Conjunctive-Query Containment and Constraint Satisfaction |
1998 |
PODS |
0.00024281448 |
| 971 |
Rewriting Aggregate Queries Using Views |
1999 |
PODS |
0.00014915911 |
| 1,056 |
Cosette: An Automated Prover for SQL |
2017 |
CIDR |
0.00014391317 |
| 1,489 |
On the Decidability of Query Containment under Constraints |
1998 |
PODS |
0.00011687823 |
| 1,520 |
The Containment Problem for Real Conjunctive Queries with Inequalities |
2006 |
PODS |
0.00011524911 |
| 1,921 |
Selecting Subexpressions to Materialize at Datacenter Scale |
2018 |
VLDB |
0.00010085899 |
| 2,097 |
Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries |
2018 |
VLDB |
9.5439744e-05 |
| 2,394 |
Algebraic Properties of Bag Data Types |
1991 |
VLDB |
8.8911581e-05 |
| 3,430 |
Demonstration of the Cosette Automated SQL Prover |
2017 |
SIGMOD |
7.0985442e-05 |
| 4,650 |
A Chase Too Far? |
2000 |
SIGMOD |
6.0169723e-05 |
| 5,710 |
Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract) |
1997 |
PODS |
5.3619696e-05 |
| 7,672 |
Query Containment in Entity SQL (Extended Abstract) |
2013 |
SIGMOD |
4.6773488e-05 |
Semantically Similar Papers
| Overall Rank |
Paper |
Year |
Venue |
Pagerank |
| 9,339 |
Local Transformations and Conjunctive-Query Equivalence |
2012 |
PODS |
4.351469e-05 |
| 5,710 |
Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract) |
1997 |
PODS |
5.3619696e-05 |
| 2,105 |
Deciding Equivalences among Aggregate Queries |
1998 |
PODS |
9.5309231e-05 |
| 12,305 |
Equivalence of SQL Queries In Presence of Embedded Dependencies |
2009 |
PODS |
4.1905499e-05 |
| 5,196 |
Equivalence of Queries Combining Set and Bag-Set Semantics |
2006 |
PODS |
5.6311982e-05 |
| 8,780 |
GEqO: ML-Accelerated Semantic Equivalence Detection |
2023 |
SIGMOD |
4.4485568e-05 |
| 4,385 |
Proving Query Equivalence Using Linear Integer Arithmetic |
2023 |
SIGMOD |
6.2247394e-05 |
| 5,245 |
QED: A Powerful Query Equivalence Decider for SQL |
2024 |
VLDB |
5.6017846e-05 |
| 2,097 |
Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries |
2018 |
VLDB |
9.5439744e-05 |
| 11,123 |
Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries |
2024 |
VLDB |
4.1905499e-05 |