Research Abstracts - 2007

Introduction

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 [1] 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.

Potential Impact

Kodkod is designed expressly as a plugin component that can easily be incorporated as a backend of another tool [2]. 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:

• Design analysis. Design specifications written for the Alloy Analyzer, including a model of the Mondex electronic purse [3], have been analyzed with Kodkod.
• Code analysis. A procedure can be checked against a declarative specification by translating its code to a relational constraint. Dennis and Chang [4] have applied this technique to check the correctness of Java data structures.
• Course scheduling. Given the prerequisite dependencies, overall requirements of a degree program, information about which terms particular courses are offered in, and a set of courses already taken, Kodkod can plan a student's course schedule. Yeung [5] has built such a course scheduling application.
• Alloy Analyzer 4.0. An ongoing project seeks to replace the core of the Alloy Analyzer with Kodkod.

Research Challenges

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:

• A new symmetry-breaking scheme that works in the presence of partial instances; the inability of Alloy's scheme to accommodate partial instances was a key reason for not supporting them.
• A new sparse-matrix representation of relations that is both simpler to implement and better performing than the `atomization' used in Alloy.
• A new scheme for detecting opportunities for sharing in the constraint abstract syntax tree inspired by boolean expression diagrams and reduced boolean circuits.

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 [1].

Figure 1. Performance of SAT-based model finders on a selection of symmetric and TPTP problems.

Acknowledgements

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).

References:

[1] Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. In The Proceedings of TACAS '07, Braga, Portugal, March 2007.

[2] Emina Torlak and Greg Dennis. Kodkod for Alloy Users. In The Proceedings of the First ACM Alloy Workshop, Portland, Oregon, November 2006.

[3] Tahina Ramananandro. The Mondex Case Study with Alloy. http://www.eleves.ens.fr/home/ramanana/work/mondex/, 2006.

[4] Greg Dennis, Felix Chang and Daniel Jackson. Modular Verifiction of Code. In The Proceedings of ISSTA '06, Portland, Maine, July 2006.

[5] Vincent Yeung. Declarative Configuration Applied to Course Scheduling. Master's thesis. Massachusetts Institute of Technology, Cambridge, MA, June 2006.