Abstracts - 2007
Kodkod: A Relational Model Finder
Emina Torlak & Daniel Jackson
Many computational problems can be expressed declaratively as collections of constraints, and then solved using a constraint-solving engine. A variety of such engines have been developed, each tailored for a particular language: resolution engines for Prolog, Simplex for linear inequalities, SAT solvers for boolean formulas, etc. This project concerns the design of a general purpose relational engine: that is, a model finder for a constraint language that combines first order logic with relational algebra and transitive closure.
Our earlier work involved the development of the Alloy modeling language and its analyzer. The Alloy Analyzer was designed for the analysis of software models, and attempts to use it as a generic relational engine have been hampered by its lack of a mechanism for exploiting a priori knowledge about a problem's solution. The user provides only a constraint to be solved, and if a partial solution--or, a partial instance--is available which the obtained solution should extend, it can be provided only in the form of additional constraints. Because the solver must essentially rediscover the partial instance from the constraints, this strategy does not scale well.
Kodkod  is a new tool that, unlike the Alloy Analyzer, is suitable as a generic relational engine. Kodkod outperforms the Analyzer dramatically on problems involving partial instances, and, due to improvements in the core technology, outperforms Alloy even on the problems for which Alloy was designed. It also outperforms other SAT-based logic engines (such as Paradox and MACE) on a variety of standard benchmarks.
Kodkod is designed expressly as a plugin component that can easily be incorporated as a backend of another tool . Unlike the Alloy Analyzer, Kodkod provides a clean Java interface for constructing, manipulating, and analyzing an Alloy formula; it allows the user to specify a partial instance of the formula; it allows common subformulas and subexpressions to be directly shared; and it employs an improved scheme for detecting further sharing opportunities.
Current applications of Kodkod include:
An efficient SAT-based model finder requires a mechanism for specifying partial solutions, an effective symmetry detection and breaking scheme, and an economical translation to boolean logic.
Symmetry detection. In the case of a standard typed logic such as the Alloy language, symmetry detection in a universe of uninterpreted atoms is straightforward: the symmetries of a problem are the permutations that map an atom in its universe to itself or to another atom of the same type. Atoms of the same type are interchangeable because Alloy provides no means of referring to individual atoms--i.e. of specifying partial instances. The Kodkod logic does, however, so even if it were typed, atoms of the same type would not necessarily be interchangeable, making the problem of symmetry detection in Kodkod as hard as graph automorphism detection.
Translation to boolean logic. The Alloy Analyzer's translation to boolean is based on the assumption that the universe of discourse is partitioned into a set of basic types. This makes it impossible for Alloy to directly translate an expression with an arbitrary set of tuples as its upper (or lower) bound--a capability necessary for handling partial instances.
Major Findings and Results
Our research yielded three novel techniques for overcoming the outlined challenges:
These techniques have been implemented and evaluated, with promising results (Figure 1). Kodkod significantly outperforms the Alloy Analyzer on problems with and without partial instances, and its performance is competitive with that of other SAT-based model finders on a variety of standard benchmarks .
This work is supported in part by the National Science Foundation (Science of Design Award 0438897 and Deep and Scalable Analysis of Software Award 0541183).
 Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. In The Proceedings of TACAS '07, Braga, Portugal, March 2007.
 Emina Torlak and Greg Dennis. Kodkod for Alloy Users. In The Proceedings of the First ACM Alloy Workshop, Portland, Oregon, November 2006.
 Tahina Ramananandro. The Mondex Case Study with Alloy. http://www.eleves.ens.fr/home/ramanana/work/mondex/, 2006.
 Greg Dennis, Felix Chang and Daniel Jackson. Modular Verifiction of Code. In The Proceedings of ISSTA '06, Portland, Maine, July 2006.
 Vincent Yeung. Declarative Configuration Applied to Course Scheduling. Master's thesis. Massachusetts Institute of Technology, Cambridge, MA, June 2006.