vZ

ν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 10 articles )

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

  1. 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)
  2. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  3. Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
  4. 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)
  5. Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
  6. Terra-Neves, Miguel; Lynce, Inês; Manquinho, Vasco: Introducing Pareto minimal correction subsets (2017)
  7. Zhang, Danfeng; Kifer, Daniel: LightDP: towards automating differential privacy proofs (2017)
  8. Candeago, Lorenzo; Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Speeding up the constraint-based method in difference logic (2016)
  9. Hyvärinen, Antti E. J.; Marescotti, Matteo; Sharygina, Natasha: Search-space partitioning for parallelizing SMT solvers (2015)
  10. Pavlinovic, Zvonimir; King, Tim; Wies, Thomas: Practical SMT-based type error localization (2015)