νZ — An Optimizing SMT Solver. νZ is a part of the SMT solver Z3. It allows users to pose and solve optimization problems modulo theories. Many SMT applications use models to provide satisfying assignments, and a growing number of these build on top of Z3 to get optimal assignments with respect to objective functions. νZ provides a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations. Objective functions are combined as either Pareto fronts, lexicographically, or each objective is optimized ndependently. We describe usage scenarios of νZ , outline the tool architecture that allows dispatching problems to special purpose solvers, and examine use cases

References in zbMATH (referenced in 14 articles )

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

  1. Bigarella, Filippo; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Jonáš, Martin; Roveri, Marco; Sebastiani, Roberto; Trentin, Patrick: Optimization modulo non-linear arithmetic via incremental linearization (2021)
  2. 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)
  3. Koehler, Jana; Bürgler, Josef; Fontana, Urs; Fux, Etienne; Herzog, Florian; Pouly, Marc; Saller, Sophia; Salyaeva, Anastasia; Scheiblechner, Peter; Waelti, Kai: Cable tree wiring -- benchmarking solvers on a real-world scheduling problem with a variety of precedence constraints (2021)
  4. Trentin, Patrick; Sebastiani, Roberto: Optimization modulo the theories of signed bit-vectors and floating-point numbers (2021)
  5. Chen, Qian Matteo; Finzi, Alberto; Mancini, Toni; Melatti, Igor; Tronci, Enrico: MILP, pseudo-Boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks (2020)
  6. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  7. Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
  8. 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)
  9. Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
  10. Terra-Neves, Miguel; Lynce, Inês; Manquinho, Vasco: Introducing Pareto minimal correction subsets (2017)
  11. Zhang, Danfeng; Kifer, Daniel: LightDP: towards automating differential privacy proofs (2017)
  12. Candeago, Lorenzo; Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Speeding up the constraint-based method in difference logic (2016)
  13. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  14. Pavlinovic, Zvonimir; King, Tim; Wies, Thomas: Practical SMT-based type error localization (2015)