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.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