Optimization Modulo Theories (OMT) is an extension of SMT, which combines SMT with optimization, findingmodels that make given objectives optimal. OMT has been extended to be incremental and to handle multiple objective functions either independently or with their linear, lexicographic, Pareto, min-max/max-min combinations.OMT applications can be found not only in the domains of Formal Verification, Automated Reasoning and Planningwith Resources, but also Machine Learning and Requirement Engineering.(Partial weighted) MAXSMT–or, alternatively, OMT with Pseudo-Boolean objective functions– is a very-relevantsubcase of OMT. Unfortunately, using general OMT algorithm for MAXSMT suffers from some intrinsic inefficiencies in some cases. In this paper we identify the sources of such inefficiencies and address them by enhancinggeneral OMT by means of sorting networks. We implemented this idea on top of the OPTIMATHSAT OMT solverand evaluated them empirically on problems coming from Machine Learning and Requirement Engineering. Theempirical results support the effectiveness of this idea.

On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT / Sebastiani, Roberto; Trentin, Patrick. - ELETTRONICO. - 1617:(2016). ((Intervento presentato al convegno SMT 2016 tenutosi a Coimbra, Portugal nel 1st-2nd July 2016.

On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT

Roberto Sebastiani;Patrick Trentin
2016

Abstract

Optimization Modulo Theories (OMT) is an extension of SMT, which combines SMT with optimization, findingmodels that make given objectives optimal. OMT has been extended to be incremental and to handle multiple objective functions either independently or with their linear, lexicographic, Pareto, min-max/max-min combinations.OMT applications can be found not only in the domains of Formal Verification, Automated Reasoning and Planningwith Resources, but also Machine Learning and Requirement Engineering.(Partial weighted) MAXSMT–or, alternatively, OMT with Pseudo-Boolean objective functions– is a very-relevantsubcase of OMT. Unfortunately, using general OMT algorithm for MAXSMT suffers from some intrinsic inefficiencies in some cases. In this paper we identify the sources of such inefficiencies and address them by enhancinggeneral OMT by means of sorting networks. We implemented this idea on top of the OPTIMATHSAT OMT solverand evaluated them empirically on problems coming from Machine Learning and Requirement Engineering. Theempirical results support the effectiveness of this idea.
Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, IJCAR 2016
Aachen
CEUR
Sebastiani, Roberto; Trentin, Patrick
On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT / Sebastiani, Roberto; Trentin, Patrick. - ELETTRONICO. - 1617:(2016). ((Intervento presentato al convegno SMT 2016 tenutosi a Coimbra, Portugal nel 1st-2nd July 2016.
File in questo prodotto:
File Dimensione Formato  
paper9.pdf

accesso aperto

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