2012 | OriginalPaper | Buchkapitel
Optimization in SMT with (ℚ) Cost Functions
verfasst von : Roberto Sebastiani, Silvia Tomasi
Erschienen in: Automated Reasoning
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 contexts of automated reasoning and formal verification, 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, bit-vectors). Surprisingly, very little work has been done to extend SMT to deal with
optimization
problems; in particular, we are not aware of any work on SMT solvers able to produce solutions which minimize cost functions over
arithmetical
variables. This is unfortunate, since some problems of interest require this functionality.
In this paper we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of
${\mathcal LA}$
(ℚ) 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 AR 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 which 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.