A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic
Authors: Fuqi Jia, Yuhang Dong, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, Jian Zhang
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 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, Opti Math SAT. ... Empirical Evaluation We implemented OCAC in CVC5 1.0.4, utilizing the Lazard projection operator (Lazard 1994; Kremer and Brandt 2021) provided by Co Co ALib (Abbott and Bigatti 2010) and Lib Poly (Jovanovic and Dutertre 2017). |
| Researcher Affiliation | Academia | 1SKLCS and Key Laboratory of System Software, ISCAS, Beijing, China 2Laboratory of Parallel Software and Computational Science, ISCAS, Beijing, China 3University of Chinese Academy of Sciences, Beijing, China 4 Stanford University, Stanford, USA 5 University of Oxford, Oxford, UK |
| Pseudocode | Yes | Algorithm 1: OCAC Input: ψ t = xt: The OMT branch formula, with n variables. Output: g, v, l: A flag that ψ t = xt is satisfiable; The optimum value; The cutting lemma. 1: I := , g := , v := None 2: while S I I I = R do 3: st := Sample Objective Value(I) 4: (T, O) := Solve Internal(ψ t = xt xt = st) 5: if T = then 6: g := , v := Analyze Cell(O) 7: O := O [st, + ) 8: end if 9: I := I {O} 10: end while 11: return (g, v, Lemma(v)) |
| Open Source Code | Yes | Supplementary https://github.com/fuqi-jia/AAAI25 |
| Open Datasets | Yes | In benchmarks generated from SMT-LIB instances, our algorithm finds the optimum value in about 150% more instances compared to the current leading solver, Opti Math SAT. ... The experimental instances are generated from satisfiable SMT(QF NRA) benchmarks. |
| Dataset Splits | No | The paper describes how instances were randomly selected and gathered for evaluation but does not specify distinct training, validation, and testing splits in the traditional sense, or standard splits with citations. |
| Hardware Specification | Yes | All experiments are done with an Intel(R) Xeon(R) CPU E5-2680 v4 @ 2.40GHz and 256G RAM within Ubuntu 20.04.6 LTS. |
| Software Dependencies | Yes | We implemented OCAC in CVC5 1.0.4, utilizing the Lazard projection operator (Lazard 1994; Kremer and Brandt 2021) provided by Co Co ALib (Abbott and Bigatti 2010) and Lib Poly (Jovanovic and Dutertre 2017). ... We use Z3 4.13.0 (de Moura and Bjørner 2008) for the first-order formulation and to verify the optimum correctness with a timeout of 1200 s. |
| Experiment Setup | Yes | The timeout for each solver that executes each instance is 1200 seconds. |