Optimizations for compiling declarative models into boolean formulas

Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang, Martin Rinard

Research output: Contribution to journalConference article

Abstract

Advances in SAT solver technology 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 paper presents our experience 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.

Original languageEnglish (US)
Pages (from-to)187-202
Number of pages16
JournalLecture Notes in Computer Science
Volume3569
StatePublished - Oct 17 2005
Event8th International Conference on Theory and Applications of Satisfiability Testing, SAT 2005 - St Andrews, United Kingdom
Duration: Jun 19 2005Jun 23 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Optimizations for compiling declarative models into boolean formulas'. Together they form a unique fingerprint.

  • Cite this

    Marinov, D., Khurshid, S., Bugrara, S., Zhang, L., & Rinard, M. (2005). Optimizations for compiling declarative models into boolean formulas. Lecture Notes in Computer Science, 3569, 187-202.