Skip to main content
SpringerLink
Log in

SqlSol: An accurate SQL Query Synthesizer

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11852))

Included in the following conference series:

Abstract

SQL is the programming language for communicating with relational databases, but writing SQL queries is challenging for many end users due to lack of programming knowledge. In this paper, we present an efficient and accurate algorithm that helps users to synthesize SQL queries from IO examples, which is the first algorithm to encode SQL synthesis problem into constraint-solving problem. We propose an axiom that encodes the semantics of a SQL query into logic constraints, and decompose the SQL synthesis problem into two parts: problem-encoding and constraint-solving. For the problem-encoding part, we use a SQL template that is same as prior work and parameterize it, then based on this axiom, we encode the parameters into logic constraints. For the constraint-solving part, we use the off-the-shelf modern SMT solvers. Our algorithm supports multiple IO examples, therefore users can add more examples to refine the solution until a correct one is found. We implemented a tool, SqlSol, and evaluated it on 171 benchmarks. The results showed that it efficiently solved 68% of the benchmarks in 3 s in average. For those SqlSol cannot solve, SqlSol terminated in 4 s in average.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Relatioal algebra. https://en.wikipedia.org/wiki/Relational_algebra

  2. Scythe. https://github.com/Mestway/Scythe

  3. SMT-COMP. https://smt-comp.github.io

  4. TIOBE. https://www.tiobe.com/tiobe-index/

  5. Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  6. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org

  7. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  8. Feng, Y., Martins, R., Van Geffen, J., Dillig, I., Chaudhuri, S.: Component-based synthesis of table consolidation and transformation tasks from examples. ACM SIGPLAN Not. 52(6), 422–436 (2017)

    Article  Google Scholar 

  9. Gulwani, S.: Dimensions in program synthesis. In: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 13–24. ACM (2010)

    Google Scholar 

  10. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. ACM SIGPLAN Not. 46(6), 62–73 (2011)

    Article  Google Scholar 

  11. Halbert, D.C.: Programming by example. Ph.D. thesis, University of California, Berkeley (1984)

    Google Scholar 

  12. Lieberman, H.: Programming by example. Commun. ACM 43(3), 72 (2000)

    Article  Google Scholar 

  13. Ramakrishnan, R., Gehrke, J.: Database Management Systems, 3rd edn. McGraw-Hill Inc., New York (2003)

    MATH  Google Scholar 

  14. Veanes, M., Tillmann, N., de Halleux, J.: Qex: symbolic SQL query explorer. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 425–446. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_24

    Chapter  Google Scholar 

  15. Wang, C., Cheung, A., Bodik, R.: Synthesizing highly expressive sql queries from input-output examples. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 452–466. ACM (2017)

    Google Scholar 

  16. Zhang, S., Sun, Y.: Automatically synthesizing SQL queries from input-output examples. In: 2013 IEEE/ACM 28th International Conference on Automated Software Engineering (ASE), pp. 224–234. IEEE (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Western Michigan University, Kalamazoo, USA

    Lin Cheng

Authors
  1. Lin Cheng
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lin Cheng .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cheng, L. (2019). SqlSol: An accurate SQL Query Synthesizer. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation