You can manage bookmarks using lists, please log in to your user account for this.
Media type:
E-Article
Title:
Optimization Modulo Theories with Linear Rational Costs
Contributor:
Sebastiani, Roberto;
Tomasi, Silvia
Published:
Association for Computing Machinery (ACM), 2015
Published in:
ACM Transactions on Computational Logic, 16 (2015) 2, Seite 1-43
Language:
English
DOI:
10.1145/2699915
ISSN:
1529-3785;
1557-945X
Origination:
Footnote:
Description:
<jats:p>
In the contexts of automated reasoning (AR) and formal verification (FV), important
<jats:italic>decision</jats:italic>
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
<jats:italic>optimization</jats:italic>
problems; in particular, we are not aware of any previous work on SMT solvers able to produce solutions that minimize cost functions over
<jats:italic>arithmetical</jats:italic>
variables. This is unfortunate, since some problems of interest require this functionality.
</jats:p>
<jats:p>
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
<jats:italic>Linear Generalized Disjunctive Programming (LGDP)</jats:italic>
, 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.
</jats:p>