A Survey of Satisfiability Modulo Theory <s> Optimization <s> 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. <s> BIB001 </s> A Survey of Satisfiability Modulo Theory <s> Optimization <s> In systems with hard real-time constraints, it is necessary to compute upper bounds on the worst-case execution time (WCET) of programs; the closer the bound to the real WCET, the better. This is especially the case of synchronous reactive control loops with a fixed clock; the WCET of the loop body must not exceed the clock period. We compute the WCET (or at least a close upper bound thereof) as the solution of an optimization modulo theory problem that takes into account the semantics of the program, in contrast to other methods that compute the longest path whether or not it is feasible according to these semantics. Optimization modulo theory extends satisfiability modulo theory (SMT) to maximization problems. Immediate encodings of WCET problems into SMT yield formulas intractable for all current production-grade solvers; this is inherent to the DPLL(T) approach to SMT implemented in these solvers. By conjoining some appropriate "cuts" to these formulas, we considerably reduce the computation time of the SMT-solver. We experimented our approach on a variety of control programs, using the OTAWA analyzer both as baseline and as underlying microarchitectural analysis for our analysis, and show notable improvement on the WCET bound on a variety of benchmarks and control programs. <s> BIB002
Instead of finding one solution, one may wish to find a solution that maximizes (or nearly so) some function f . A simple approach is binary search: provided one can get a lower bound l and an upper bound h on the maximum f ( x * ), one queries the solver for a solution x such that f ( x) ≥ m, where m = l+h 2 ; if such a solution is found, refine the lower bound l := f ( x) and restart, otherwise h := m and restart. Proceed until l = h. This converges in finite time if f has integer value. This approach has been successfully applied to e.g. worst-case execution time problems BIB002 . In the case of LRA (resp. LIA), optimization generalizes linear programming (resp. linear integer programming) to formulas with disjunctions. In fact, linear programming can be applied locally to a polyhedron of solutions: when a DPLL(T) solver finds a solution x of a formula F , it also finds a conjunction C of atoms such that C ⇒ F ; C defines a polyhedron and one can optimize within it, until a local optimum x l . Then one adds the constraint f ( x) > f ( x l ) and restart; the last x l found is the optimum (one can also detected unboundedness). This approach can never enumerate the same C (or subsets thereof) twice and thus must terminate. It may, however, scan an exponential number of useless C's; it may be combined with binary search for best effect BIB001 .