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
- 11823
- Venue
- VLDB
- Year
- 2019
- Pagerank
- 6.6499845e-05
- Overall Rank
- 3,901 | 72.87%
- 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,596 |
WeTune: Automatic Discovery and Verification of Query Rewrite Rules |
2022 |
SIGMOD |
8.4729982e-05 |
| 3,606 |
EVA: A Symbolic Approach to Accelerating Exploratory Video Analytics with Materialized Views |
2022 |
SIGMOD |
6.9260354e-05 |
| 3,625 |
Cost Models for Big Data Query Processing: Learning, Retrofitting, and Our Findings |
2020 |
SIGMOD |
6.9055212e-05 |
| 4,388 |
Proving Query Equivalence Using Linear Integer Arithmetic |
2023 |
SIGMOD |
6.2303078e-05 |
| 4,664 |
Efficient Answering of Historical What-if Queries |
2022 |
SIGMOD |
6.0127053e-05 |
| 5,243 |
QED: A Powerful Query Equivalence Decider for SQL |
2024 |
VLDB |
5.6071695e-05 |
| 7,139 |
Automated Validating and Fixing of Text-to-SQL Translation with Execution Consistency |
2025 |
SIGMOD |
4.821174e-05 |
| 7,283 |
Sia: Optimizing Queries using Learned Predicates |
2021 |
SIGMOD |
4.7764688e-05 |
| 8,345 |
SlabCity: Whole-Query Optimization using Program Synthesis |
2023 |
VLDB |
4.5426916e-05 |
| 8,645 |
Predicate Pushdown for Data Science Pipelines |
2023 |
SIGMOD |
4.4772518e-05 |
| 8,783 |
GEqO: ML-Accelerated Semantic Equivalence Detection |
2023 |
SIGMOD |
4.452825e-05 |
| 9,623 |
Qr-Hint: Actionable Hints Towards Correcting Wrong SQL Queries |
2024 |
SIGMOD |
4.3161663e-05 |
| 10,568 |
QOVIS: Understanding and Diagnosing Query Optimizer via a Visualization-assisted Approach |
2025 |
VLDB |
4.1945683e-05 |
| 10,762 |
ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation |
2025 |
VLDB |
4.1945683e-05 |
| 11,220 |
Lightweight Materialization for Fast Dashboards Over Joins |
2023 |
SIGMOD |
4.1945683e-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.00027036073 |
| 407 |
Conjunctive-Query Containment and Constraint Satisfaction |
1998 |
PODS |
0.00024004562 |
| 971 |
Rewriting Aggregate Queries Using Views |
1999 |
PODS |
0.00014925576 |
| 1,057 |
Cosette: An Automated Prover for SQL |
2017 |
CIDR |
0.0001439886 |
| 1,490 |
On the Decidability of Query Containment under Constraints |
1998 |
PODS |
0.00011699154 |
| 1,522 |
The Containment Problem for Real Conjunctive Queries with Inequalities |
2006 |
PODS |
0.0001153051 |
| 1,922 |
Selecting Subexpressions to Materialize at Datacenter Scale |
2018 |
VLDB |
0.00010082599 |
| 2,099 |
Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries |
2018 |
VLDB |
9.5479391e-05 |
| 2,395 |
Algebraic Properties of Bag Data Types |
1991 |
VLDB |
8.8998019e-05 |
| 3,432 |
Demonstration of the Cosette Automated SQL Prover |
2017 |
SIGMOD |
7.1008151e-05 |
| 4,654 |
A Chase Too Far? |
2000 |
SIGMOD |
6.022356e-05 |
| 5,697 |
Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract) |
1997 |
PODS |
5.3671336e-05 |
| 7,674 |
Query Containment in Entity SQL (Extended Abstract) |
2013 |
SIGMOD |
4.6818255e-05 |
Semantically Similar Papers
| Overall Rank |
Paper |
Year |
Venue |
Pagerank |
| 9,334 |
Local Transformations and Conjunctive-Query Equivalence |
2012 |
PODS |
4.3556432e-05 |
| 5,697 |
Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract) |
1997 |
PODS |
5.3671336e-05 |
| 2,103 |
Deciding Equivalences among Aggregate Queries |
1998 |
PODS |
9.5385023e-05 |
| 12,297 |
Equivalence of SQL Queries In Presence of Embedded Dependencies |
2009 |
PODS |
4.1945683e-05 |
| 5,195 |
Equivalence of Queries Combining Set and Bag-Set Semantics |
2006 |
PODS |
5.6366303e-05 |
| 8,783 |
GEqO: ML-Accelerated Semantic Equivalence Detection |
2023 |
SIGMOD |
4.452825e-05 |
| 4,388 |
Proving Query Equivalence Using Linear Integer Arithmetic |
2023 |
SIGMOD |
6.2303078e-05 |
| 5,243 |
QED: A Powerful Query Equivalence Decider for SQL |
2024 |
VLDB |
5.6071695e-05 |
| 2,099 |
Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries |
2018 |
VLDB |
9.5479391e-05 |
| 11,120 |
Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries |
2024 |
VLDB |
4.1945683e-05 |