Solving Floating-Point Constraints with Continuous Optimization
summary
Grater converts floating‑point formulas into continuous, piecewise‑linear objective functions and uses gradient descent with random starts to find global minima; each candidate undergoes a three‑step validation (gradient exists and is zero, objective equals zero, original formula holds). On SMT‑LIB and JFS benchmarks Grater solves as many problems as Bitwuzla and CVC5 (and one more than CVC5 in one suite) while running over 10× faster on average and 30–50× faster in median time across hard benchmarks.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:45Floating-point constraints overview
- 2:52MCMC limitations
- 3:33Gradient descent for optimization
- 4:59Workflow demo
- 8:08Objective function design
- 10:59Translation and solver
- 12:49Implementation and evaluation
- 14:37Advantages and contributions
- 15:19Q&A with ExaRt author
- 16:44Audience discussion
related talks
18mScalable Floating-Point Satisfiability via Staged Optimization
01h 07mOptimization Crash Course (continued)
46mSmooth Nonconvex Min-Max Optimization
01h 28mFollow the gradient: an introduction to mathematical optimisation
25mEfficient Local Search for Nonlinear Real Arithmetic
01h 18mOptimization I
13mProgram Analysis via Efficient Symbolic Abstraction
19mSMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories