A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic

Abstract

Optimization Modulo Nonlinear Real Arithmetic, abbreviated as OMT(NRA), generally focuses on optimizing a given objective subject to quantifier-free Boolean combinations of primitive constraints, including Boolean variables, polynomial equations, and inequalities. It is widely applicable in areas like program verification, analysis, planning, and so on. The existing solver, OptiMathSAT, officially supporting OMT(NRA), employs an incomplete algorithm. We present a sound and complete algorithm, Optimization Cylindrical Algebraic Covering (OCAC), integrated within the Conflict-Driven Clause Learning (CDCL) framework, specifically tailored for OMT(NRA) problems. We establish the correctness and termination of CDCL(OCAC) and explore alternative approaches using cylindrical algebraic decomposition (CAD) and first-order formulations. Our work includes the development of the first complete OMT solver for NRA, demonstrating significant performance improvements. In benchmarks generated from SMT-LIB instances, our algorithm finds the optimum value in about 150% more instances compared to the current leading solver, OptiMathSAT.