{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T03:20:05Z","timestamp":1783567205884,"version":"3.55.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,12,8]],"date-time":"2023-12-08T00:00:00Z","timestamp":1701993600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62272304,62132014"],"award-info":[{"award-number":["62272304,62132014"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"National Science Foundation","doi-asserted-by":"publisher","award":["FMitF-2220407,CCF-2131476"],"award-info":[{"award-number":["FMitF-2220407,CCF-2131476"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Manag. Data"],"published-print":{"date-parts":[[2023,12,8]]},"abstract":"<jats:p>Proving the equivalence between SQL queries is a fundamental problem in database research. Existing solvers model queries using algebraic representations and convert such representations into first-order logic formulas so that query equivalence can be verified by solving a satisfiability problem. The main challenge lies in \"unbounded summations\", which appear commonly in a query's algebraic representation in order to model common SQL features, such as projection and aggregate functions. Unfortunately, existing solvers handle unbounded summations in an ad-hoc manner based on heuristics or syntax comparison, which severely limits the set of queries that can be supported.<\/jats:p>\n          <jats:p>This paper develops a new SQL equivalence prover called SQLSolver, which can handle unbounded summations in a principled way. Our key insight is to use the theory of LIA^*, which extends linear integer arithmetic formulas with unbounded sums and provides algorithms to translate a LIA^* formula to a LIA formula that can be decided using existing SMT solvers. We augment the basic LIA^* theory to handle several complex scenarios (such as nested unbounded summations) that arise from modeling real-world queries. We evaluate SQLSolver with 359 equivalent query pairs derived from the SQL rewrite rules in Calcite and Spark SQL. SQLSolver successfully proves 346 pairs of them, which significantly outperforms existing provers.<\/jats:p>","DOI":"10.1145\/3626768","type":"journal-article","created":{"date-parts":[[2023,12,12]],"date-time":"2023-12-12T14:01:21Z","timestamp":1702389681000},"page":"1-26","source":"Crossref","is-referenced-by-count":14,"title":["Proving Query Equivalence Using Linear Integer Arithmetic"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8138-8639","authenticated-orcid":false,"given":"Haoran","family":"Ding","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0220-5726","authenticated-orcid":false,"given":"Zhaoguo","family":"Wang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5303-2599","authenticated-orcid":false,"given":"Yicun","family":"Yang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9009-9503","authenticated-orcid":false,"given":"Dexin","family":"Zhang","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7868-6615","authenticated-orcid":false,"given":"Zhenglin","family":"Xu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9720-0361","authenticated-orcid":false,"given":"Haibo","family":"Chen","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-0776","authenticated-orcid":false,"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9574-1746","authenticated-orcid":false,"given":"Jinyang","family":"Li","sequence":"additional","affiliation":[{"name":"New York University, New York, NY, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,12,12]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Foundations of databases","author":"Abiteboul Serge","unstructured":"Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of databases. Vol. 8. Addison-Wesley Reading."},{"key":"e_1_2_2_2_1","unstructured":"amcintosh. 2013. Query featuring outer joins behaves differently in oracle 12c. http:\/\/stackoverflow.com\/questions\/19686262."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3190662"},{"key":"e_1_2_2_4_1","volume-title":"The calculus of computation: decision procedures with applications to verification","author":"Bradley Aaron R","unstructured":"Aaron R Bradley and Zohar Manna. 2007. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media."},{"key":"e_1_2_2_5_1","unstructured":"Apache Calcite. 2021. Calcite Test Suite. https:\/\/ipads.se.sjtu.edu.cn:1312\/opensource\/wetune\/-\/blob\/main\/wtune_data\/calcite\/calcite_tests."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803397"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/153850.153856"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3035918.3058728"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.14778\/3236187.3236200"},{"key":"e_1_2_2_10_1","unstructured":"Shumo Chu Brendan Murphy Jared Roesch Alvin Cheung and Dan Suciu. 2018b. UDP source code. https:\/\/github.com\/uwdb\/Cosette\/tree\/master\/uexp."},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the 8th Biennial Conference on Innovative Data Systems Research","author":"Chu Shumo","year":"2017","unstructured":"Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017b. Cosette: An Automated Prover for SQL.. In Proceedings of the 8th Biennial Conference on Innovative Data Systems Research (Chaminade, California, USA) (CIDR '17)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062348"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1219092.1219093"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/303976.303992"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_16_1","unstructured":"Visweswara Sai Prashanth Dintyala Arpit Narechania and Joy Arulraj. to appear. SQLCheck: Automated Detection and Diagnosis of SQL Anti-Patterns. ( to appear)."},{"key":"e_1_2_2_17_1","unstructured":"The Apache Software Foundation. 2023. Spark SQL. https:\/\/github.com\/apache\/spark\/tree\/master\/sql."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/38714.38723"},{"key":"e_1_2_2_19_1","first-page":"19","article-title":"The cascades framework for query optimization","volume":"18","author":"Graefe Goetz","year":"1995","unstructured":"Goetz Graefe. 1995. The cascades framework for query optimization. IEEE Data Eng. Bull., Vol. 18, 3 (1995), 19--29.","journal-title":"IEEE Data Eng. Bull."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE.1993.344061"},{"key":"e_1_2_2_21_1","unstructured":"Carnegie Mellon Database Research Group. 2023 a. Multi-DBMS SQL Benchmarking Framework via JDBC. https:\/\/github.com\/cmu-db\/benchbase\/tree\/main\/src\/main\/java\/com\/oltpbenchmark\/benchmarks\/tpcc."},{"key":"e_1_2_2_22_1","unstructured":"Carnegie Mellon Database Research Group. 2023 b. Multi-DBMS SQL Benchmarking Framework via JDBC. https:\/\/github.com\/cmu-db\/benchbase\/tree\/main\/src\/main\/java\/com\/oltpbenchmark\/benchmarks\/tpch."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/211414.211419"},{"key":"e_1_2_2_24_1","unstructured":"ISO. 2016. ISO\/IEC 9075--2:2016. https:\/\/www.iso.org\/standard\/63556.html."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142363"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the 9th Biennial Conference on Innovative Data Systems Research","author":"Kipf Andreas","year":"2019","unstructured":"Andreas Kipf, Thomas Kipf, Bernhard Radke, Viktor Leis, Peter Boncz, and Alfons Kemper. 2019. Learned cardinalities: Estimating correlated joins with deep learning. In Proceedings of the 9th Biennial Conference on Innovative Data Systems Research (Asilomar, California, USA) (CIDR '19)."},{"key":"e_1_2_2_27_1","volume-title":"Learning to optimize join queries with deep reinforcement learning. arXiv preprint arXiv:1808.03196","author":"Krishnan Sanjay","year":"2018","unstructured":"Sanjay Krishnan, Zongheng Yang, Ken Goldberg, Joseph Hellerstein, and Ion Stoica. 2018. Learning to optimize join queries with deep reinforcement learning. arXiv preprint arXiv:1808.03196 (2018)."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_20"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39322-9_17"},{"key":"e_1_2_2_31_1","volume-title":"Neo: A learned query optimizer. arXiv preprint arXiv:1904.03711","author":"Marcus Ryan","year":"2019","unstructured":"Ryan Marcus, Parimarjan Negi, Hongzi Mao, Chi Zhang, Mohammad Alizadeh, Tim Kraska, Olga Papaemmanouil, and Nesime Tatbul. 2019. Neo: A learned query optimizer. arXiv preprint arXiv:1904.03711 (2019)."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211954.3211957"},{"key":"e_1_2_2_33_1","volume-title":"Proceedings of the 9th Biennial Conference on Innovative Data Systems Research","author":"Marcus Ryan","year":"2019","unstructured":"Ryan Marcus and Olga Papaemmanouil. 2019. Towards a Hands-Free Query Optimizer through Deep Learning. In Proceedings of the 9th Biennial Conference on Innovative Data Systems Research (Asilomar, California, USA) (CIDR '19)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645918.756653"},{"key":"e_1_2_2_35_1","unstructured":"Terence Parr. 2020. ANTLR v4. https:\/\/github.com\/antlr\/antlr4."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","unstructured":"Ruzica Piskac. 2011. Decision Procedures for Program Synthesis and Verification. (2011) 200. https:\/\/doi.org\/10.5075\/epfl-thesis-5220","DOI":"10.5075\/epfl-thesis-5220"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_20"},{"key":"e_1_2_2_38_1","volume-title":"Decision Procedures for Multisets with Cardinality Constraints (VMCAI'08)","author":"Piskac Ruzica","unstructured":"Ruzica Piskac and Viktor Kuncak. 2008b. Decision Procedures for Multisets with Cardinality Constraints (VMCAI'08). Springer-Verlag, Berlin, Heidelberg, 218--232."},{"key":"e_1_2_2_39_1","volume-title":"Linear Arithmetic with Stars","author":"Piskac Ruzica","unstructured":"Ruzica Piskac and Viktor Kuncak. 2008c. Linear Arithmetic with Stars. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 268--280."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322221"},{"key":"e_1_2_2_41_1","unstructured":"David Schmitt. 2010. Optimizer creates strange execution plan leading to wrong results. http:\/\/tinyurl.com\/hwwn53r."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/645927.672349"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514221.3526125"},{"key":"e_1_2_2_44_1","unstructured":"Zhaoguo Wang Zhou Zhou Yicun Yang Haoran Ding Gansen Hu Ding Ding Chuzhe Tang Haibo Chen and Jinyang Li. 2022b. WeTune source code. https:\/\/ipads.se.sjtu.edu.cn:1312\/opensource\/wetune."},{"key":"e_1_2_2_45_1","unstructured":"Qi Zhou Joy Arulraj Shamkant Navathe William Harris and Jinpeng Wu. 2020. SPES source code. https:\/\/github.com\/georgia-tech-db\/spes."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.14778\/3342263.3342267"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDE53745.2022.00250"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.14778\/3485450.3485456"}],"container-title":["Proceedings of the ACM on Management of Data"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626768","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626768","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T13:00:38Z","timestamp":1755867638000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626768"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,8]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12,8]]}},"alternative-id":["10.1145\/3626768"],"URL":"https:\/\/doi.org\/10.1145\/3626768","relation":{},"ISSN":["2836-6573"],"issn-type":[{"value":"2836-6573","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,8]]}}}