Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. OptiMathSAT is an OMT solver which 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 (partial weighted) MaxSMT . Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min–max /max–min combinations. OptiMathSAT provides an incremental interface, it supports both an extended version of the SMT-LIBv2 language and a subset of the FlatZinc language, and can be interfaced via an API. In this paper we describe OptiMathSAT and its usage in full detail.

OptiMathSAT: A Tool for Optimization Modulo Theories / Sebastiani, Roberto; Trentin, Patrick. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 64:(2020), pp. 423-460. [10.1007/s10817-018-09508-6]

OptiMathSAT: A Tool for Optimization Modulo Theories

Sebastiani, Roberto;Trentin, Patrick
2020

Abstract

Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. OptiMathSAT is an OMT solver which 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 (partial weighted) MaxSMT . Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min–max /max–min combinations. OptiMathSAT provides an incremental interface, it supports both an extended version of the SMT-LIBv2 language and a subset of the FlatZinc language, and can be interfaced via an API. In this paper we describe OptiMathSAT and its usage in full detail.
Sebastiani, Roberto; Trentin, Patrick
OptiMathSAT: A Tool for Optimization Modulo Theories / Sebastiani, Roberto; Trentin, Patrick. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 64:(2020), pp. 423-460. [10.1007/s10817-018-09508-6]
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Pre-print non referato (Non-refereed preprint)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.33 MB
Formato Adobe PDF
1.33 MB Adobe PDF Visualizza/Apri
Sebastiani-Trentin2018_Article_OptiMathSATAToolForOptimizatio.pdf

Solo gestori archivio

Descrizione: Versione online first
Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 3.32 MB
Formato Adobe PDF
3.32 MB Adobe PDF   Visualizza/Apri
Sebastiani-Trentin2020_Article_OptiMathSATAToolForOptimizatio.pdf

Solo gestori archivio

Descrizione: Versione editoriale finale
Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 3.31 MB
Formato Adobe PDF
3.31 MB 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/225416
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 11
social impact