A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic

Authors

  • Fuqi JiaInstitute of Software, Chinese Academy of SciencesUniversity of the Chinese Academy of Sciences
  • Yuhang DongInstitute of Software, Chinese Academy of SciencesUniversity of the Chinese Academy of Sciences
  • Rui HanInstitute of Software, Chinese Academy of SciencesUniversity of the Chinese Academy of Sciences
  • Pei HuangStanford University
  • Minghao LiuUniversity of Oxford
  • Feifei MaInstitute of Software, Chinese Academy of SciencesUniversity of the Chinese Academy of Sciences
  • Jian ZhangInstitute of Software, Chinese Academy of SciencesUniversity of the Chinese Academy of Sciences

DOI:

https://doi.org/10.1609/aaai.v39i11.33224

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.
AAAI-25 / IAAI-25 / EAAI-25 Proceedings Cover

Downloads

Published

2025-04-11

How to Cite

Jia, F., Dong, Y., Han, R., Huang, P., Liu, M., Ma, F., & Zhang, J. (2025). A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic.Proceedings of the AAAI Conference on Artificial Intelligence,39(11), 11255-11263. https://doi.org/10.1609/aaai.v39i11.33224

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization