In the contexts of automated reasoning (AR) and formal verification (FV), important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade, efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, and bit vectors). Surprisingly, little work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any previous work on SMT solvers able to produce solutions that minimize cost functions over arithmetical variables. This is unfortunate, since some problems of interest require this functionality. In the work described in this article we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of linear rational cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in the AR, FV, and SMT domains, we have experimentally evaluated our implementation against state-of-the-art tools for the domain of Linear Generalized Disjunctive Programming (LGDP), which is closest in spirit to our domain, on sets of problems that have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach. Categories and Subject Descriptors: F.4.1 [ Mathematical Logic and Formal Languages]: Mathematical Logic—Mechanical theorem proving General Terms: Theory, Algorithms, Performance Additional Key Words and Phrases: Satisfiability modulo theories, automated reasoning, optimization.

Optimization Modulo Theories with Linear Rational Costs / Sebastiani, Roberto; Tomasi, Silvia. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - STAMPA. - 2015:16, 2(2015), pp. 1201-1243. [10.1145/2699915]

Optimization Modulo Theories with Linear Rational Costs

Sebastiani, Roberto;Tomasi, Silvia
2015-01-01

Abstract

In the contexts of automated reasoning (AR) and formal verification (FV), important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade, efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, and bit vectors). Surprisingly, little work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any previous work on SMT solvers able to produce solutions that minimize cost functions over arithmetical variables. This is unfortunate, since some problems of interest require this functionality. In the work described in this article we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of linear rational cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in the AR, FV, and SMT domains, we have experimentally evaluated our implementation against state-of-the-art tools for the domain of Linear Generalized Disjunctive Programming (LGDP), which is closest in spirit to our domain, on sets of problems that have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach. Categories and Subject Descriptors: F.4.1 [ Mathematical Logic and Formal Languages]: Mathematical Logic—Mechanical theorem proving General Terms: Theory, Algorithms, Performance Additional Key Words and Phrases: Satisfiability modulo theories, automated reasoning, optimization.
2015
16, 2
Sebastiani, Roberto; Tomasi, Silvia
Optimization Modulo Theories with Linear Rational Costs / Sebastiani, Roberto; Tomasi, Silvia. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - STAMPA. - 2015:16, 2(2015), pp. 1201-1243. [10.1145/2699915]
File in questo prodotto:
File Dimensione Formato  
a12-sebastiani.pdf

Solo gestori archivio

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