The Satisfiability Modulo Theory (SMT) problem over
floating-point operations presents a significant challenge.
State-of-the-art SMT solvers often run into difficulties when
dealing with large, complex floating-point
constraints. Recently, a new approach to floating-point constraint solving
emerges, utilizing mathematical optimization (MO) methods
as an engine of their solving approach.

Despite the novelty, these  
methods can fall short in both effectiveness and efficiency  
due to issues of the translated functions (e.g., discontinuity) and  
inherent limitations of their underlying MO method (e.g.,  
imprecise search process, scalability issues). 

Driven by these weaknesses of prior solvers, this paper introduces  
a new MO-based approach that is shown highly potent in solving  
floating-point constraints. Specifically,  
on the benchmarks of \textsf{JFS} (a recent solver based on fuzzing), \textsf{Grater},  
a realization of our approach, solves as many constraints as \textsf{Bitwuzla} 
and one more than \textsf{CVC5} but runs over 10 times faster and over 40 times 
faster than \textsf{Bitwuzla} and \textsf{CVC5} in median solving time across  
all benchmarks. It is worth mentioning that \textsf{Bitwuzla} and \textsf{CVC5} are the strongest solvers  
for floating-point constraints according to results of the annual international  
SMT solver competition (SMT-COMP). Together, they have won all gold medals  
for \textit{QF\_FPArith} and \textit{FPArith}  
divisions, which focus on floating-point constraints solving, over the past three years. 
To further evaluate \textsf{Grater}, we select over  
100 most difficult benchmarks from the \textit{FP} SMT-LIB, a logic regularly used in SMT-COMP. 
The difficulty is measured by the complexity of the composition  
(e.g., number of variables, clauses) and the interdependencies within constraints.  
\textsf{Grater} again solves the same number of constraints as \textsf{Bitwuzla} and \textsf{CVC5} while running  
over 10 times faster than both solvers in average solving time, and over 50 times  
(resp. 30 times) faster than \textsf{Bitwuzla} (resp. \textsf{CVC5}) in median solving time.  
 

We release the source code of \textsf{Grater}, along with all evaluation data,  
including detailed comparisons of \textsf{Grater} against each baseline solver (i.e., \textsf{Z3}, 
\textsf{CVC5}, \textsf{Bitwuzla}, \textsf{JFS}, \textsf{XSat}, and \textsf{CoverMe}), at  
\url{https://github.com/grater-exp/grater-experiment} to facilitate reproducibility.