Abstract

In the contexts of Formal Verification (FV) and Automated Reasoning (AR), Satisfiability Modulo Theories (SMT) is an important discipline that allows for dealing with industrial-level decision problems. Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories with the ability to express, and optimize, objective functions. Recently, there has been a growing interest towards OMT, as witnessed by an increasing number of applications using, at their core, some OMT solver as main power-horse engine. However, at present few OMT solvers exist, and the development of OMT technology is still at an early stage, with large margins of improvement. We identify two major advancement directions in particular. First, there is a general need for closing the expressiveness gap with respect to SMT, and provide optimization procedures that can deal with the wider range of theories supported by SMT solvers. Second, there is an urgent need for more efficient techniques that can improve on the performance of state-of-the-art OMT solvers, because solving an OMT problem is inherently more expensive than dealing with its SMT counterpart, often by at least one order of magnitude. In this dissertation, we present a variety of techniques that deal with the identified issues and advance both the expressiveness and the efficiency of OMT. We describe our implementation of these techniques inside OptiMathSAT, a state-of-the-art OMT solver based on MathSAT5, along with its high-level architecture, Input/Output interfaces and configurable options. Thanks to our novel contributions, OptiMathSAT can now deal with the single- and the multi-objective incremental optimization of goals defined over multiple domains –the Boolean, the mixed Linear Integer and Rational Arithmetic, the Bit-Vector and the Floating Point domain– including (Partial Weighted) MaxSMT. We validate our theoretical contributions experimentally, by comparing the performance of OptiMathSAT against other, competing, OMT solvers. Finally, we investigate the effectiveness of OMT beyond the scope of Formal Verification, and describe an experimental evaluation comparing OptiMathSAT with Finite Domain Constraint Programming tools on benchmark-sets coming from their respective domains.