Efficient Local Search for Nonlinear Real Arithmetic
summary
An efficient local-search solver for full nonlinear real arithmetic implements incremental variable scores (boundaries of make/break intervals) and temporary equality relaxation (replace exact equalities by ±ε then restore exact values), adds candidate-move selection and a look‑ahead when no critical move exists, and runs in C++ over floating/rational value types. The implementation solves many satisfiable NRA benchmarks that MCSAT-based SMT solvers struggle with and is competitive on satisfiable instances; experiments report more solved equality‑heavy cases after relaxation and successful restores to exact solutions.
AI-written summary · about
chapters (10)
- 0:00Local search for nonlinear arithmetic
- 1:52Local search framework
- 4:19Critical move procedure
- 7:42Traditional score computation
- 12:27Temporary equality relaxation
- 15:27Restoring relaxed constraints
- 16:31Implementation details
- 17:34Experimental results
- 19:00Conclusion
- 20:28Question and answer session
related talks
19mSolving Floating-Point Constraints with Continuous Optimization
13mMind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
31mLearning in Games with Best-Response Oracles
12mEquilibrium Computation and the Foundations of Multi-Agent Machine Learning
57mRethinking Binary Search: Improving on a Classic with AI Assistance
17mSynthesizing MILP Constraints for Efficient and Robust Optimization
52mLearning as a Tool for Algorithm Design and Beyond-Worst-Case Analysis
46mFaster SDP Hierarchy Solvers for Local Rounding Algorithms