Optimization Modulo Theories with Linear Rational Costs

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, bit-vectors). Surprisingly, little work has been done to extend SMT to deal with optimization problems; in particular, concerning the development of SMT solvers able to produce solutions which minimize cost functions over arithmetical variables (we are aware of only one very-recent work [Li et al., POPL-14]). In the work described in this thesis 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 AR and FV, 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, and a very-recent SMT-based optimizer [Li et al., POPL-14]. Our benchmark set consists of problems which have been previously proposed for our competitors. The results show that our tool is very competitive, and often outperforms these tools (especially LGDP ones)on their problems, clearly demonstrating the potential of the approach. Stochastic Local-Search (SLS) procedures are sometimes very competitive in pure SAT on both satisfiable instances and optimization problems. As a side work, in this thesis we investigate the possibility to exploit SLS inside SMT tools which are commonly based on the lazy approach (it combines a Conflict-Driven-Clause-Learning(CDCL)SAT solver with theory-specific decision procedures, called T-solvers). We first introduce a general procedure for integrating a SLS solver of the WalkSAT family with a T-solver. Then we present a group of techniques aimed at improving the synergy between these two components. Finally we implement all these techniques into a novel SLS-based SMT solver for the theory of linear arithmetic over the rationals, and perform an empirical evaluation on satisfiable instances. Although the results are encouraging, we concluded that the efficiency of proposed SLS-based SMT techniques is still far from being comparable to that of standard SMT solvers.