Dissertation
Extensions to theories of relations and tables in SMT
University of Iowa
Doctor of Philosophy (PhD), University of Iowa
Summer 2025
DOI: 10.25820/etd.008098
Abstract
Problems from many industrial applications can be encoded naturally in the languages of finite sets and multisets. Concrete examples include software design specifications, ontologies, relational algebra, database queries, normative requirements, and authorization policies. To reason about these languages, researchers have developed several specialized solvers for the quantifier-free first-order formulas for sets, relations, and multisets and implemented them in SMT solvers. Solvers based on Satisfiability Modulo Theories (SMT) have proven to be particularly effective at reasoning about these kinds of problems. However, some applications require more expressive power than the ones offered by these solvers. One class of examples is represented by modeling languages with set-bounded quantifiers, that is, quantified variables ranging over finite sets. Constraints written in these languages have been proven hard to solve using general quantification techniques in SMT solvers. Another class of examples is languages based on relational algebra such as Alloy and SQL which generate constraints containing second-order operators, such as filter and map, not supported by existing solvers. This thesis proposes a general approach that extends existing relational solvers in SMT with a number of first-order and second-order operators to handle encodings of these languages efficiently.
For the first class, it proposes extending a quantifier-free fragment of relations with a filter operator and using it to encode set-bounded quantifiers. The thesis discusses an extension of a relational SMT solver with support for the filter operator. Experimental results show that this extension outperforms other quantification techniques in satisfiable problems generated by SLEEC, a tool based on relational logic for modeling normative behavior, such as requirements in healthcare. The extension is also very competitive on unsatisfiable problems when compared to LEGOS, a specialized solver for SLEEC. The thesis additionally identifies a class of constraints with restricted applications of the filter operator whose satisfiability is decidable. It also shows that such restrictions are necessary because unrestricted applications make the satisfiability problem undecidable.
For the second class of languages, this thesis adds further operators such as map and prov jection and uses them to encode SQL queries based on finite set semantics. To support queries with multisets semantics, the thesis introduces a theory of tables with filter and map operators as an extension to a theory of finite multisets. Since SQL supports null values in tables, the thesis introduces a theory of nullable sorts based on an extension of the theory of algebraic datatypes. The thesis integrates novel specialized solvers for the theories above into cvc5, an SMT solver that already supports reasoning in a large number of theories including the theories of arithmetic, datatypes and strings. This extended combination of theories enables a uniform encoding of several classes of SQL verification problems such as query emptiness, containment, and equivalence. Experimental results show this approach is competitive in proving equivalence of two queries in a fragment of SQL language based on set semantics. It provides counterexamples for inequivalent queries based on either set or bag semantics.
Details
- Title: Subtitle
- Extensions to theories of relations and tables in SMT
- Creators
- Mudathir Mohamed
- Contributors
- Cesare Tinelli (Advisor)Andrew Reynolds (Committee Member)Garrett Morris (Committee Member)Katherine Kosaian (Committee Member)Alberto Maria Segre (Committee Member)
- Resource Type
- Dissertation
- Degree Awarded
- Doctor of Philosophy (PhD), University of Iowa
- Degree in
- Computer Science
- Date degree season
- Summer 2025
- DOI
- 10.25820/etd.008098
- Publisher
- University of Iowa
- Number of pages
- xiv, 156 pages
- Copyright
- Copyright 2025 Mudathir Mohamed
- Language
- English
- Date submitted
- 07/07/2025
- Description illustrations
- Illustrations, tables, graphs, charts
- Description bibliographic
- Includes bibliographical references (pages 150-156).
- Public Abstract (ETD)
Relational databases are the backbone of many business applications like banking, accounting and health computer systems. They are mainly used to store and retrieve data, organized in tables, from dedicated servers or from the cloud. Examples of tables in a health system are patients, doctors, appointments, visits, etc. To query data from these tables, a Structured Query Language (SQL) is used to retrieve individual records like visit summary, or comprehensive reports like the number of patients per month in the current year. Performance is a crucial requirement for SQL queries. Two queries can be written to retrieve the same data, but they differ in their execution time due to several factors including physical structure of tables, and types of computation applied to them. Therefore, queries are usually rewritten either manually by database developers or automatically by cloud systems to improve execution time. Rewriting queries is complex and error-prone. Therefore, there is a need to automatically verify that those rewritten queries are equivalent to the original ones, the main goal of this thesis. Here we extend existing theories for sets and bags to support reasoning about SQL queries with either bag or set semantics. The difference between bag and set semantics is duplicate records are allowed in bag semantics, while they are disallowed in set semantics. We also present a theory of nullables to reason about null values which represent unknown and missing values. We designed and implemented solvers for these theories and evaluated them on a set of benchmarks derived from public sets of SQL equivalence problems.
- Academic Unit
- Computer Science
- Record Identifier
- 9984948540102771
Metrics
1 File views/ downloads
12 Record Views