vZ swMATH ID: 22666 Software Authors: N. Bjørner, A.-D. Phan, L. Fleckenstein Description: ν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 Homepage: https://link.springer.com/chapter/10.1007/978-3-662-46681-0_14 Dependencies: Z3 Related Software: z3; OptiMathSAT; SYMBA; MathSAT5; SMT-LIB; Yices; GitHub; CPLEX; MiniSat; CVC4; MiniZinc; Sat4j; LogMIP; CVC; dReal; CHUFFED; OR-tools; STP; UppSAT; Boolector Cited in: 14 Publications all top 5 Cited by 55 Authors 3 Sebastiani, Roberto 3 Trentin, Patrick 2 Larraz, Daniel 2 Oliveras, Albert 2 Rodríguez-Carbonell, Enric 2 Rubio, Albert 1 Alhiyafi, Jamal 1 Bigarella, Filippo 1 Borralleras, Cristina 1 Bürgler, Josef 1 Candeago, Lorenzo 1 Chen, Li 1 Chen, Liqian 1 Chen, Qian Matteo 1 Cimatti, Alessandro 1 Eraşcu, Mădălina 1 Finzi, Alberto 1 Fontana, Urs 1 Fux, Etienne 1 Griggio, Alberto 1 Herzog, Florian 1 Hyvärinen, Antti E. J. 1 Irfan, Ahmed 1 Jiang, Jiahong 1 Jonáš, Martin 1 Kifer, Daniel 1 King, Tim 1 Köhler, Jana 1 Lynce, Inês 1 Lyu, Yinrun 1 Mancini, Toni 1 Manquinho, Vasco M. 1 Marescotti, Matteo 1 Melatti, Igor 1 Micota, Flavia 1 Min-Allah, Nasro 1 Pavlinovic, Zvonimir 1 Pouly, Marc 1 Roveri, Marco 1 Saller, Sophia 1 Salyaeva, Anastasia 1 Scheiblechner, Peter 1 Sharygina, Natasha 1 Terra-Neves, Miguel 1 Tronci, Enrico 1 Waelti, Kai 1 Wang, Chong 1 Wang, Ji 1 Wang, Yongji 1 Wies, Thomas 1 Wu, Jingzheng 1 Wu, Xueguang 1 Zaharie, Daniela 1 Zhang, Changyou 1 Zhang, Danfeng all top 5 Cited in 6 Serials 2 Journal of Automated Reasoning 1 Journal of Global Optimization 1 Constraints 1 Fundamenta Informaticae 1 ACM Transactions on Computational Logic 1 Journal of Logical and Algebraic Methods in Programming Cited in 3 Fields 13 Computer science (68-XX) 5 Operations research, mathematical programming (90-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year