Many SMT problems of interest may require the capability of finding models that are optimal wrt. some objective functions. These problems are grouped under the umbrella term of Optimization Modulo Theories -- OMT. In this paper we present OptiMathSAT, an OMT tool extending the M ATH SAT5 SMT solver. OptiMathSAT allows for solving a list of optimization problems on SMT formulas with linear objective functions --on the Boolean, the rational and the integer domains, and on their combination thereof-- including MaxSMT. Multiple objective functions can be combined together and handled either independently, or lexicographically, or in a min-max/max-min fashion. OptiMathSAT ships with an extended SMT-LIB V 2 input syntax and C API bindings, and it preserves the incremental attitude of its underlying SMT solver.

OptiMathSAT: A Tool for Optimization Modulo Theories / Sebastiani, Roberto; Trentin, Patrick. - STAMPA. - 9206:(2015), pp. 447-454. ((Intervento presentato al convegno 27th International Conference CAV 2015 tenutosi a San Francisco, CA nel 18th-24th July 2015 [10.1007/978-3-319-21690-4_27].

OptiMathSAT: A Tool for Optimization Modulo Theories

Sebastiani, Roberto;Trentin, Patrick
2015

Abstract

Many SMT problems of interest may require the capability of finding models that are optimal wrt. some objective functions. These problems are grouped under the umbrella term of Optimization Modulo Theories -- OMT. In this paper we present OptiMathSAT, an OMT tool extending the M ATH SAT5 SMT solver. OptiMathSAT allows for solving a list of optimization problems on SMT formulas with linear objective functions --on the Boolean, the rational and the integer domains, and on their combination thereof-- including MaxSMT. Multiple objective functions can be combined together and handled either independently, or lexicographically, or in a min-max/max-min fashion. OptiMathSAT ships with an extended SMT-LIB V 2 input syntax and C API bindings, and it preserves the incremental attitude of its underlying SMT solver.
Computer Aided Verification 27th International Conference CAV 2015 Proceedings Part 1
Cham
Springer
978-3-319-21689-8
978-3-319-21690-4
Sebastiani, Roberto; Trentin, Patrick
OptiMathSAT: A Tool for Optimization Modulo Theories / Sebastiani, Roberto; Trentin, Patrick. - STAMPA. - 9206:(2015), pp. 447-454. ((Intervento presentato al convegno 27th International Conference CAV 2015 tenutosi a San Francisco, CA nel 18th-24th July 2015 [10.1007/978-3-319-21690-4_27].
File in questo prodotto:
File Dimensione Formato  
cav15-1.pdf

embargo fino al 31/12/2016

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 184.33 kB
Formato Adobe PDF
184.33 kB Adobe PDF Visualizza/Apri
Sebastiani-Trentin2015_Chapter_OptiMathSATAToolForOptimizatio.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 522.04 kB
Formato Adobe PDF
522.04 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/115805
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 63
  • ???jsp.display-item.citation.isi??? 48
social impact