νZ - An Optimizing SMT Solver
作者： Nikolaj Bjørner , Anh-Dung Phan , Lars Fleckenstein
DOI: 10.1007/978-3-662-46681-0_14
关键词:
摘要: ν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 …
springer.com
sci-hub.st 参考文章(13)
Nina Narodytska, Fahiem Bacchus, Maximum satisfiability using core-guided MAXSAT resolution national conference on artificial intelligence. pp. 2717- 2723 ,(2014)
Klaus Becker, Bernhard Schätz, Michael Armbruster, Christian Buckl, A Formal Model for Constraint-Based Deployment Calculation and Analysis for Fault-Tolerant Systems international conference on software engineering. pp. 205- 219 ,(2014) , 10.1007/978-3-319-10431-7_15
Jessica Davies, Fahiem Bacchus, Postponing Optimization to Speed Up MAXSAT Solving principles and practice of constraint programming. pp. 247- 262 ,(2013) , 10.1007/978-3-642-40627-0_21
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints principles and practice of constraint programming. pp. 80- 96 ,(2013) , 10.1007/978-3-642-40627-0_9
Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio, Proving Non-termination Using Max-SMT computer aided verification. pp. 779- 796 ,(2014) , 10.1007/978-3-319-08867-9_52
Robert Nieuwenhuis, Albert Oliveras, On SAT Modulo Theories and Optimization Problems Lecture Notes in Computer Science. pp. 156- 169 ,(2006) , 10.1007/11814948_18
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico, Satisfiability Modulo the Theory of Costs: Foundations and Applications Tools and Algorithms for the Construction and Analysis of Systems. pp. 99- 113 ,(2010) , 10.1007/978-3-642-12002-2_8
Roberto Sebastiani, Silvia Tomasi, Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions Automated Reasoning. pp. 484- 498 ,(2012) , 10.1007/978-3-642-31365-3_38
Antonio Morgado, Federico Heras, Joao Marques-Silva, Improvements to core-guided binary search for MaxSAT theory and applications of satisfiability testing. pp. 284- 297 ,(2012) , 10.1007/978-3-642-31612-8_22