vZ - Maximal Satisfaction with Z3

Nikolaj Bjørner, Phan Anh Dung

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Satisfiability Modulo Theories, SMT, solvers are used in many applications. These applications benefit from the power of tuned and scalable theorem proving technologies for supported logics and specialized theory solvers. SMT solvers are primarily used to determine whether formulas are satisfiable. Furthermore, when formulas are satisfiable, many applications need models that assign values to free variables. Yet, in many cases arbitrary assignments are insufficient, and what is really needed is an optimal assignment with respect to objective functions. So far, users of Z3, an SMT solver from Microsoft Research, build custom loops to achieve objective values. This is no longer necessary with νZ (new-Z, or max-Z), an extension within Z3 that lets users formulate objective functions directly with Z3. Under the hood there is 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 independently.
Original languageEnglish
Title of host publicationProceedings of the 6th International Symposium on Symbolic Computation in Software Science (SCSS 2014)
Number of pages10
Publication date2015
Publication statusPublished - 2015
Event6th International Symposium on Symbolic Computation in Software Science (SCSS 2014) - Gammarth, Tunisia
Duration: 7 Dec 20148 Dec 2014
Conference number: 6
http://www.easychair.org/smart-program/SCSS2014/index.html

Conference

Conference6th International Symposium on Symbolic Computation in Software Science (SCSS 2014)
Number6
CountryTunisia
CityGammarth
Period07/12/201408/12/2014
Internet address

Fingerprint Dive into the research topics of 'vZ - Maximal Satisfaction with Z3'. Together they form a unique fingerprint.

Cite this