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 few 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 LA(Q) cost functions, combining SMT with standard minimization techniques. We have implemented the proposed approach within the MathSAT SMT solver. Due to the lack of competitors in AR and SMT domains, we 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.
Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
Department of Electrical and Computer Engineering, National University of Singapore, Singapore（电子与计算机工程系，新加坡国立大学）；School of Computing and Data Science, The University of Hong Kong, Hong Kong, China（计算与数据科学学院，香港大学）
Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis
Department of Management Information Systems, National ChengChi University, Taipei, Taiwan（管理信息系，中华大学，台北，台湾）；Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan（电子工程系，台湾大学，台北，台湾）
