Allealle: Bounded relational model finding with unbounded data

Jouke Stoel, Tijs Van Der Storm*, Jurgen J. Vinju

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Relational model finding is a successful technique which has been used in a wide range of problems during the last decade. This success is partly due to the fact that many problems contain relational structures which can be explored using relational model finders. Although these model finders allow for the exploration of such structures they often struggle with incorporating the non-relational elements. In this paper we introduce AlleAlle, a method and language that integrates reasoning on both relational structure and non-relational elements —the data— of a problem. By combining first order logic with Codd’s relational algebra, transitive closure, and optimization criteria, we obtain a rich input language for expressing constraints on both relational and scalar values. We present the semantics of AlleAlle and the translation of AlleAlle specifications to SMT constraints, and use the off-the-shelf SMT solver Z3 to find solutions. We evaluate AlleAlle by comparing its performance with Kodkod, a state-of-the-art relational model finder, and by encoding a solution to the optimal package resolution problem. Initial benchmarking show that although the translation times of AlleAlle can be improved, the resulting SMT constraints can efficiently be solved by the underlying solver.
Original languageEnglish
Title of host publicationOnward! 2019
Subtitle of host publicationProceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2019
PublisherAssociation for Computing Machinery, Inc
Pages46-61
Number of pages16
ISBN (Print)9781450369954
DOIs
Publication statusPublished - 23-Oct-2019
EventSymposium on New Ideas in Programming and Reflections on Software (Onward!) - Athene, Greece
Duration: 22-Oct-201929-Oct-2019

Publication series

NameOnward! 2019 - Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2019

Conference

ConferenceSymposium on New Ideas in Programming and Reflections on Software (Onward!)
CountryGreece
CityAthene
Period22/10/201929/10/2019

Keywords

  • Constraint optimization problems
  • Constraint problems
  • First order logic
  • Model finding
  • Relational algebra
  • SMT solvers

Cite this