Symbolic optimization with SMT solvers. The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in software verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness for a bug) or proving unsatisfiability/validity (e.g., proving that a subtyping relation holds). We are often interested in finding not just an arbitrary satisfying assignment, but one that optimizes (minimizes/maximizes) certain criteria. For example, we might be interested in detecting program executions that maximize energy usage (performance bugs), or synthesizing short programs that do not make expensive API calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities. In this paper, we present SYMBA, an efficient SMT-based optimization algorithm for objective functions in the theory of linear real arithmetic (LRA). Given a formula φ and an objective function t, SYMBA finds a satisfying assignment of φ that maximizes the value of t. SYMBA utilizes efficient SMT solvers as black boxes. As a result, it is easy to implement and it directly benefits from future advances in SMT solvers. Moreover, SYMBA can optimize a set of objective functions, reusing information between them to speed up the analysis. We have implemented SYMBA and evaluated it on a large number of optimization benchmarks drawn from program analysis tasks. Our results indicate the power and efficiency of SYMBA in comparison with competing approaches, and highlight the importance of its multi-objective-function feature.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Eraşcu, Mădălina; Micota, Flavia; Zaharie, Daniela: Scalable optimal deployment in the cloud of component-based applications using optimization modulo theory, mathematical programming and symmetry breaking (2021)
  2. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theories of signed bit-vectors and floating-point numbers (2021)
  3. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  4. Cardelli, Luca; Tribastone, Mirco; Tschaikowski, Max; Vandin, Andrea: Symbolic computation of differential equivalences (2019)
  5. Lyu, Yinrun; Chen, Li; Zhang, Changyou; Qu, Dacheng; Min-Allah, Nasro; Wang, Yongji: An interleaved depth-first search method for the linear optimization problem with disjunctive constraints (2018)
  6. Shankar, Natarajan: Combining model checking and deduction (2018)
  7. Chen, Li; Lyu, Yinrun; Wang, Chong; Wu, Jingzheng; Zhang, Changyou; Min-Allah, Nasro; Alhiyafi, Jamal; Wang, Yongji: Solving linear optimization over arithmetic constraint formula (2017)
  8. Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
  9. Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea: Structured learning modulo theories (2017)
  10. Ábrahám, Erika; Kremer, Gereon: Satisfiability checking: theory and applications (2016)
  11. Vandin, Andrea; Tribastone, Mirco: Quantitative abstractions for collective adaptive systems (2016)
  12. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  13. Li, Yi; Albarghouthi, Aws; Kincaid, Zachary; Gurfinkel, Arie; Chechik, Marsha: Symbolic optimization with SMT solvers (2014)