SqlSol: An accurate SQL Query Synthesizer

摘要

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.