Research Abstracts - 2006

KodKod: Solving Formulas with Partial Instances

Emina Torlak

Introduction

Kodkod is an efficient SAT-based model finder for first order logic with relations, transitive closure, and partial instances. The current prototype is being used to verify Java code (Mana Taghdiri and Greg Dennis), plan students' schedules (Vincent Yeung), and configure communication networks (Sanjai Narain).

Approach

Like the Alloy Analyzer, Kodkod is essentially a compiler. It translates first order logic formulas (created via Kodkod API calls) into a boolean formula. The boolean formula is handed to a SAT solver, and Kodkod translates the solution into an instance of the analyzed formula, expressed as a binding of relations to values. All problems are defined over a bounded, user-specified universe.

Unlike the Alloy Analyzer, Kodkod is designed to take advantage of partial instance information, by allowing the user to specify a partial solution that the model finder then completes. In a network configuration problem, for example, the set of all active nodes is known. Any solution to a formula encoding the configuration problem must include all active nodes. The binding from the relation representing active nodes to the set of all active nodes is therefore a partial instance of the configuration formula.

Results

KodKod incorporates several new variations of the scalability techniques implemented in the Alloy Analyzer [2]. Alloy's sharing detection scheme is replaced with a new mechanism based on Boolean Expression Diagrams [1], and a new symmetry detection algorithm that accounts for partial instances has been developed and implemented. Experiments on a wide range of models show that the SAT input generated by KodKod is significantly more compact than that of the Alloy Analyzer, resulting in shorter solving times and the ability to handle larger scopes.

Research Support

This research was funded by the SoD Collaborative Research (Constraint-based Architecture Evaluation) grant from the ITR program of the National Science Foundation, and by the Model-Based Cognitive Systems for Air-Traffic Control Identification and Safety grant from Defense Advanced Research Projects Agency Cognitive Systems Program.

References:

[1] Henrik R. Andersen and Henrik Hulgaard. Boolean Expression Diagrams. In The Proceedings of LICS '97, Warszawa, Poland, June 1997.

[2] Ilya Shlyakhter. Declarative symbolic pure logic model checking. MIT PhD thesis, Cambridge, MA, February 2005.