Relational Constraint Solving in SMT

by Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett
Abstract:
Relational logic is useful for reasoning about computational problems with relational structures, including high-level system design, architectural con- figurations of network systems, ontologies, and verification of programs with linked data structures. We present a modular extension of an earlier calculus for the theory of finite sets to a theory of finite relations with such operations as transpose, product, join, and transitive closure. We implement this extension as a theory solver of the SMT solver CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling use cases. For instance, native support for relations enables a natural mapping from Alloy, a declarative modeling language based on first-order relational logic, to SMT constraints. It also enables a natural encoding of several description logics with concrete domains, allowing the use of an SMT solver to analyze, for instance, Web Ontology Language (OWL) models. We provide an initial evaluation of our solver on a number of Alloy and OWL models which shows promising results.
Reference:
Relational Constraint Solving in SMT (Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett), In Proceedings of the 26th International Conference on Automated Deduction (CADE ’17) (Leonardo de Moura, ed.), Springer, volume 10395, 2017. (Gothenburg, Sweden)
Bibtex Entry:
@inproceedings{MRT+17,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/MRT+17.pdf",
  author    = "Baoluo Meng and Andrew Reynolds and Cesare Tinelli and Clark Barrett",
  title     = "Relational Constraint Solving in SMT",
  booktitle = "Proceedings of the 26th International Conference on Automated Deduction (CADE '17)",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 10395,
  publisher = "Springer",
  editor    = "Leonardo de Moura",
  pages     = "148--165",
  month     = aug,
  year      = 2017,
  note      = "Gothenburg, Sweden",
  category  = "Conference Publications",
  abstract  = "Relational logic is useful for reasoning about computational problems
with relational structures, including high-level system design, architectural con-
figurations of network systems, ontologies, and verification of programs with
linked data structures. We present a modular extension of an earlier calculus
for the theory of finite sets to a theory of finite relations with such operations
as transpose, product, join, and transitive closure. We implement this extension
as a theory solver of the SMT solver CVC4. Combining this new solver with
the finite model finding features of CVC4 enables several compelling use cases.
For instance, native support for relations enables a natural mapping from Alloy,
a declarative modeling language based on first-order relational logic, to SMT
constraints. It also enables a natural encoding of several description logics with
concrete domains, allowing the use of an SMT solver to analyze, for instance,
Web Ontology Language (OWL) models. We provide an initial evaluation of our
solver on a number of Alloy and OWL models which shows promising results."
}

Fork me on GitHub