Optimizations for Compiling Declarative Models into Boolean Formulas

Abstract:
Advances in propositional satisfiability (SAT) have enabled many
automated analysis and reasoning tools to reduce their input problem
to a SAT problem and then to use an efficient SAT solver to solve the
underlying analysis or reasoning problem.  The solving time for SAT
solvers can vary substantially for semantically identical SAT problems
depending on how the problem is expressed.  This property motivates
the development of new optimization techniques whose goal is to
produce more efficiently solvable SAT problems, thereby improving the
overall performance of the analysis or reasoning tool.

This talk will present our experience in using several mechanical
techniques that enable the Alloy Analyzer to generate optimized SAT
formulas from first-order logic formulas.  These techniques are
inspired by similar techniques from the field of optimizing compilers,
suggesting the potential presence of underlying connections between
optimization problems from two very different domains. Our
experimental results show that our techniques can deliver substantial
performance improvement results--in some cases, they reduce the
solving time by an order of magnitude.

This is a joint work with Sarfraz Khurshid (UT Austin), Suhabe Bugrara
(MIT), Lintao Zhang (MSR), and Martin Rinard (MIT).

This talk will also briefly present the Department of Computer Science
at the University of Illinois at Urbana-Champaign.

Short biography:

Darko Marinov is an Assistant Professor in the Department of Computer
Science at the University of Illinois at Urbana-Champaign.  He was a
grad student in the CS & AI Lab at MIT, where he co-led the MulSaw
project and received a Ph.D. in 2004 and an S.M. in 2000.  He received
a B.S. from the School of Electrical Engineering at the University of
Belgrade in 1997.  His main research interests are in Software
Engineering and Programming Languages.  He is interested in rich
specification languages and checking code conformance, both
dynamically and statically.  He is also interested in compilers,
particularly in correctness of analyses and optimizations.