Satisfiability modulo relations: theory and applications

• Main Author: Meng, Baoluo
• Other Authors: Tinelli, C. (Cesare)
• Format: Others
• Language: English
• Published: University of Iowa 2018
• Subjects: Alloy; Sets and Relations; SMT; Computer Sciences
• Online Access: https://ir.uiowa.edu/etd/6614; https://ir.uiowa.edu/cgi/viewcontent.cgi?article=8113&context=etd

Many computational problems require reasoning about relational structures. Examples include high-level system design, architectural configuration of network systems, reasoning about ontologies, and verification of programs with linked data structures. Traditionally, relational models are translated to propositional formulas and then solved by leveraging SAT solvers. However, SAT solvers can only reason about problems within a finite scope, i.e, concrete cardinality bounds on the relations involved. SMT solvers, on the other hand, are efficient tools that can check automatically the satisfiability of complex constraints over several domains without scope restrictions. They are used as the back-end solvers in many verification tools. To break the limitation of bounded analysis, this thesis presents a many-sorted relational logic in SMT where relations of arity n are defined as sets of n-tuples with parametrized sorts for tuple elements. We define a version of this logic as a first-order theory of finite relations where relation terms are built from relation constants and variables, set operators, and relational operators such as join, transpose, product, and transitive closure. We also present a deductive calculus for that theory and provide proofs of refutation soundness and model soundness of our calculus. In addition, we implement the calculus as a relational solver in the SMT solver CVC4, expanding its already large set of built-in theories, and evaluate the relational solver in two applications: Alloy and Ontology, showing promising results. Moreover, with the goal of improving the performance of SMT solvers in general, we present a symmetry detection algorithm to detect symmetries in SMT formulas and present a symmetry breaking algorithm to generate blocking constraints that eliminate those symmetries. We then discuss an experimental evaluation of our implementation of these algorithms in CVC4 against SMT-LIB benchmarks.