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 13th International Symposium on Frontiers of Combining Systems, 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-01-01

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.
2021
Frontiers of Combining Systems: 13th International Symposium Proceedings
GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND
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 13th International Symposium on Frontiers of Combining Systems, 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

Open Access dal 01/01/2023

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: https://hdl.handle.net/11572/320565
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
  • OpenAlex ND
social impact