Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems on the theories of non-linear arithmetic over the reals and the integers. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions. In this paper, we show how incremental linearization can be extended to OMT in a simple way, producing an incomplete though effective OMT procedure. We describe the main ideas and algorithms, we provide an implementation within the OptiMathSAT OMT solver, and perform an empirical evaluation. The results support the effectiveness of the approach.

Optimization Modulo Non-linear Arithmetic via Incremental Linearization / Bigarella, F.; Cimatti, A.; Griggio, A.; Irfan, A.; Jonas, M.; Roveri, M.; Sebastiani, R.; Trentin, P.. - 12941:(2021), pp. 213-231. ((Intervento presentato al convegno FroCoS 2021, co-located with the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021 tenutosi a Birmingham, UK nel 8th-10th September 2021 [10.1007/978-3-030-86205-3_12].

Optimization Modulo Non-linear Arithmetic via Incremental Linearization

Cimatti A.;Griggio A.;Irfan A.;Roveri M.;Sebastiani R.;Trentin P.
2021

Abstract

Incremental linearization is a conceptually simple, yet effective, technique that we have recently proposed for solving SMT problems on the theories of non-linear arithmetic over the reals and the integers. Optimization Modulo Theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions. In this paper, we show how incremental linearization can be extended to OMT in a simple way, producing an incomplete though effective OMT procedure. We describe the main ideas and algorithms, we provide an implementation within the OptiMathSAT OMT solver, and perform an empirical evaluation. The results support the effectiveness of the approach.
Frontiers of Combining Systems: 13th International Symposium Proceedings
Cham, CH
Springer Nature Switzerland
978-3-030-86204-6
978-3-030-86205-3
Bigarella, F.; Cimatti, A.; Griggio, A.; Irfan, A.; Jonas, M.; Roveri, M.; Sebastiani, R.; Trentin, P.
Optimization Modulo Non-linear Arithmetic via Incremental Linearization / Bigarella, F.; Cimatti, A.; Griggio, A.; Irfan, A.; Jonas, M.; Roveri, M.; Sebastiani, R.; Trentin, P.. - 12941:(2021), pp. 213-231. ((Intervento presentato al convegno FroCoS 2021, co-located with the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021 tenutosi a Birmingham, UK nel 8th-10th September 2021 [10.1007/978-3-030-86205-3_12].
File in questo prodotto:
File Dimensione Formato  
main.pdf

embargo fino al 31/12/2022

Tipologia: Pre-print non referato (Non-refereed preprint)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 872.39 kB
Formato Adobe PDF
872.39 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: http://hdl.handle.net/11572/320565
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact