Optimization Modulo Theory (OMT) is an important extension of Satisfiability Modulo Theory (SMT), aiming to find models that satisfy constraints while optimizing objective functions. OMT naturally arises in program analysis and formal methods, making OMT solving an important and challenging task. OptiMathSAT is currently the state-of-the-art OMT solver supporting floating-point theories. It incrementally calls an SMT solver to prune the search space step by step until the optimal objective value is found. However, this frequent invocation of the SMT solver is highly inefficient. Therefore, this paper proposes a novel hybrid method consisting of two stages: coarse search and precise search. The coarse search stage quickly finds an approximate optimal model using an optimization search algorithm. The precise search stage then performs an SMT-based binary search starting from the approximate model to find the true optimal model (the OMT solution). Evidently, this hybrid approach reduces computational cost by rapidly shrinking the search space, thereby improving overall solving performance. We evaluated our method on benchmarks derived from SMT-LIB2 and real-world programs. Experimental results show that our method outperforms the current state-of-the-art in both effectiveness and efficiency.
Yang et al. (Mon,) studied this question.