Paper Info
Title
AlleAlle: bounded relational model finding with unbounded data
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.
Year
DOI
Venue
2019
10.1145/3359591.3359726
Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
Keywords
Field
DocType
First order logic, SMT solvers, constraint optimization problems, constraint problems, model finding, relational algebra
Algebra,Computer science,Relational model,Bounded function
Conference
ISBN
Citations 
PageRank 
978-1-4503-6995-4
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Jouke Stoel101.01
Tijs van der Storm261.13
Jurgen J. Vinju384358.95