Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions

摘要: In the contexts of automated reasoning and formal verification, important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). last decade efficient SMT solvers have been developed for several theories practical interest (e.g., linear arithmetic, arrays, bit-vectors). Surprisingly, very little work has done to extend deal with optimization problems; in particular, we not aware any on able produce solutions which minimize cost functions over arithmetical variables. This is unfortunate, since some require this functionality. In paper start filling gap. We present discuss two general procedures leveraging handle minimization ${\mathcal LA}$ (ℚ) functions, combining standard techniques. implemented within MathSAT solver. Due absence competitors AR domains, experimentally evaluated our implementation against state-of-the-art tools domain generalized disjunctive programming (LGDP), closest spirit domain, sets previously proposed as benchmarks latter tools. The results show that tool competitive with, often outperforms, these problems, clearly demonstrating potential approach.