2015 | OriginalPaper | Buchkapitel
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
verfasst von : R. Sebastiani, P. Trentin
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding models that are
optimal
wrt. some cost functions. In previous work, namely
Optimization Modulo Theory with Linear Rational Cost Functions – OMT(
$\mathcal{LRA}\cup \mathcal{T}$
), we have leveraged SMT solving to handle the
minimization
of cost functions on linear arithmetic over the rationals, by means of a combination of SMT and LP minimization techniques.
In this paper we push the envelope of our OMT approach along three directions: first, we extend it to work with linear arithmetic on the mixed integer/rational domain, by means of a combination of SMT, LP and ILP minimization techniques; second, we develop a
multi-objective
version of OMT, so that to handle many cost functions simultaneously or lexicographically; third, we develop an
incremental
version of OMT, so that to exploit the incrementality of some OMT-encodable problems. An empirical evaluation performed on OMT-encoded verification problems demonstrates the usefulness and efficiency of these extensions.