Research map / Learning theory and algorithms / Combinatorial and search optimization
A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Presents OCAC, a sound and complete cylindrical-algebraic-covering-based optimization procedure integrated into CDCL(T) for OMT(NRA), implemented in CVC5 and compared against OptiMathSAT, CAD, and first-order baselines.
Problem
Optimization modulo nonlinear real arithmetic (OMT(NRA)) requires finding optima that may be irrational, infinitesimally close to a value, or unbounded; the existing solver OptiMathSAT uses an incomplete algorithm that cannot handle many of these cases.
Approach
Converts the objective into a variable and uses cylindrical algebraic covering (CAC) with a projection operator inside CDCL(T) to sample and prune objective intervals, returning the optimum as a real root or an open-boundary value (c+ε, ±∞), with proofs of correctness and termination.
Key results
- CDCL(OCAC) solves 7932 satisfiable instances versus 3166 for OptiMathSAT(Bin), about 150.5% more.
- CDCL(OCAC) solves 1250 instances with infinity optima, and 369 and 981 in the RAN and RAN+ε categories, where OptiMathSAT solves none.
- OptiMathSAT is best on unsatisfiable instances (5040 vs 5019 for CDCL(OCAC)).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use CDCL(OCAC) instead of OptiMathSAT (Bin) | OMT(NRA) solving · SMT(QF NRA) satisfiable instances | solved instances: 150.5% more instances | Helped |
| Use CDCL(OCAC) instead of OptiMathSAT (Lin) | OMT(NRA) solving · SMT(QF NRA) satisfiable instances | solved instances: 157.3% more instances | Helped |
| Use OptiMathSAT instead of CDCL(OCAC) | OMT(NRA) solving · SMT(QF NRA) unsatisfiable instances | solved instances: 5019 -> 5040 | Helped |
| Use CDCL(OCAC) instead of CDCL(CAD) | OMT(NRA) solving · SMT(QF NRA) satisfiable instances | solved instances: 5718 -> 7932 | Helped |
Surprising findings
- FOL baseline is faster than CDCL(OCAC) in the first roughly 0.2 seconds on satisfiable instances.
Limitations
- No standardized OMT benchmarks, so evaluation relies on randomly generated instances from SMT-LIB QF_NRA.
- Only instances with up to 29 variables are solved; scalability to larger instances is limited.
- Worst-case complexity is doubly exponential in the number of variables.
Experimental setup
Datasets: SMT-LIB QF_NRA benchmarks
Benchmarks: OMT instances generated from SMT-LIB QF_NRA
Metrics: number of solved instances solving time
Baselines: OptiMathSAT (Bin) OptiMathSAT (Lin) CDCL(CAD) First-order formulation (FOL)
Builds on: cylindrical algebraic covering CDCL(T) cylindrical algebraic decomposition incremental linearization
Closest papers by meaning
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.84)
- Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization (AAAI 2025 · similarity 0.84)
- Unifying Decision and Function Queries in Stochastic Boolean Satisfiability (AAAI 2024 · similarity 0.80)
- Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits (ICML 2025 · similarity 0.80)
- OccamLLM: Fast and Exact Language Model Arithmetic in a Single Step (NeurIPS 2024 · similarity 0.80)
- OpenMathInstruct-2: Accelerating AI for Math with Massive Open-Source Instruction Data (ICLR 2025 · similarity 0.80)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.