Automated Verification of Query Equivalence Using Satisfiability Modulo Theories

Summary: EQUITAS translates SQL with complex predicates and three-valued logic into first-order formulas, using SMT to verify semantic equivalence. It handles more pairs 27× faster than algebraic methods and finds redundancy in 11% of 17,461 MaxCompute queries. (summarized by gpt-5.6-luna on Jul 24 2026)

Paper ID: 12011
Venue: VLDB
Year: 2019
Pagerank: 7.518491e-05
Overall Rank: 3,327 | 77.18%
DOI: 10.14778/3342263.3342267

Incoming Non-self Citations Over Time

Authors

1. Qi Zhou (Georgia Institute of Technology)
2. Joy Arulraj (Georgia Institute of Technology)
3. Shamkant Navathe (Georgia Institute of Technology)
4. William Harris (Galois Inc)
5. Dong Xu (Alibaba)

BibTeX Citation

@article{zhou_vldb19,
        title = {{Automated Verification of Query Equivalence Using Satisfiability Modulo Theories}},
        author = {Zhou, Qi and Arulraj, Joy and Navathe, Shamkant and Harris, William and Xu, Dong},
        journal = {PVLDB},
        series = {{VLDB} '19},
        volume = {12},
        number = {11},
        pages = {1276--1288},
        doi = {10.14778/3342263.3342267},
        url = {https://doi.org/10.14778/3342263.3342267},
        year = {2019}
}

Incoming Citations (Sorted by Pagerank)

Showing 15 of 15 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank
1,982	WeTune: Automatic Discovery and Verification of Query Rewrite Rules	2022	SIGMOD	9.3573897e-05
2,822	Cost Models for Big Data Query Processing: Learning, Retrofitting, and Our Findings	2020	SIGMOD	8.0898536e-05
2,933	EVA: A Symbolic Approach to Accelerating Exploratory Video Analytics with Materialized Views	2022	SIGMOD	7.9474026e-05
3,769	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD	7.1403543e-05
4,805	Efficient Answering of Historical What-if Queries	2022	SIGMOD	6.5003306e-05
5,353	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB	6.2519268e-05
6,031	Sia: Optimizing Queries using Learned Predicates	2021	SIGMOD	6.0007422e-05
6,267	Automated Validating and Fixing of Text-to-SQL Translation with Execution Consistency	2025	SIGMOD	5.9348282e-05
8,164	SlabCity: Whole-Query Optimization using Program Synthesis	2023	VLDB	5.4750309e-05
8,465	Predicate Pushdown for Data Science Pipelines	2023	SIGMOD	5.4194578e-05
8,798	GEqO: ML-Accelerated Semantic Equivalence Detection	2023	SIGMOD	5.3698781e-05
8,834	Qr-Hint: Actionable Hints Towards Correcting Wrong SQL Queries	2024	SIGMOD	5.3599176e-05
9,945	ParSEval: Plan-aware Test Database Generation for SQL Equivalence Evaluation	2025	VLDB	5.1915905e-05
10,834	QOVIS: Understanding and Diagnosing Query Optimizer via a Visualization-assisted Approach	2025	VLDB	5.093636e-05
11,421	Lightweight Materialization for Fast Dashboards Over Joins	2023	SIGMOD	5.093636e-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
309	Optimization of Real Conjunctive Queries	1993	PODS	0.00021768596
382	Conjunctive-Query Containment and Constraint Satisfaction	1998	PODS	0.00019546431
869	Rewriting Aggregate Queries Using Views	1999	PODS	0.00013503594
910	Cosette: An Automated Prover for SQL	2017	CIDR	0.00013285905
1,269	The Containment Problem for Real Conjunctive Queries with Inequalities	2006	PODS	0.000113935
1,630	On the Decidability of Query Containment under Constraints	1998	PODS	0.00010180625
1,765	Selecting Subexpressions to Materialize at Datacenter Scale	2018	VLDB	9.8079546e-05
1,829	Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries	2018	VLDB	9.6671311e-05
2,423	Algebraic Properties of Bag Data Types	1991	VLDB	8.6016807e-05
3,172	Demonstration of the Cosette Automated SQL Prover	2017	SIGMOD	7.6679093e-05
4,426	A Chase Too Far?	2000	SIGMOD	6.7098324e-05
5,643	Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract)	1997	PODS	6.1379759e-05
7,593	Query Containment in Entity SQL (Extended Abstract)	2013	SIGMOD	5.5893275e-05

Semantically Similar Papers

#	Overall Rank	Paper	Year	Venue
1	9,483	Local Transformations and Conjunctive-Query Equivalence	2012	PODS
2	5,643	Conjunctive Query Equivalence of Keyed Relational Schemas (Extended Abstract)	1997	PODS
3	2,238	Deciding Equivalences among Aggregate Queries	1998	PODS
4	12,492	Equivalence of SQL Queries In Presence of Embedded Dependencies	2009	PODS
5	5,062	Equivalence of Queries Combining Set and Bag-Set Semantics	2006	PODS
6	8,798	GEqO: ML-Accelerated Semantic Equivalence Detection	2023	SIGMOD
7	3,769	Proving Query Equivalence Using Linear Integer Arithmetic	2023	SIGMOD
8	5,353	QED: A Powerful Query Equivalence Decider for SQL	2024	VLDB
9	1,829	Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries	2018	VLDB
10	11,326	Demonstration of the VeriEQL Equivalence Checker for Complex SQL Queries	2024	VLDB