Scalable Floating-Point Satisfiability via Staged Optimization

• URL: http://arxiv.org/abs/2601.04492v1
• Date: Thu, 08 Jan 2026 01:51:46 GMT
• Title: Scalable Floating-Point Satisfiability via Staged Optimization
• Authors: Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran,
• Abstract summary: This work introduces StageSAT, a new approach to solving floating-point satisfiability.<n>StageSAT reframes a floating-point formula as a series of optimization problems in three stages of increasing precision.
• Score: 4.212975258164135
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This work introduces StageSAT, a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages of increasing precision. It begins with a fast, projection-aided descent objective to guide the search toward a feasible region, proceeding to bit-level accuracy with ULP$^2$ optimization and a final $n$-ULP lattice refinement. By construction, the final stage uses a representing function that is zero if and only if a candidate satisfies all constraints. Thus, when optimization drives the objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness. To improve search, StageSAT introduces a partial monotone descent property on linear constraints via orthogonal projection, preventing the optimizer from stalling on flat or misleading landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions; it treats complex arithmetic as a black-box, using runtime evaluations to navigate the input space. We implement StageSAT and evaluate it on extensive benchmarks, including SMT-COMP'25 suites and difficult cases from prior work. StageSAT proved more scalable and accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget, finding most satisfiable instances without producing spurious models. This amounts to 99.4% recall on satisfiable cases with 0% false SAT, exceeding the reliability of prior optimization-based solvers. StageSAT also delivered significant speedups (often 5--10$\times$) over traditional bit-precise SMT and numeric solvers. These results demonstrate that staged optimization significantly improves performance and correctness of floating-point satisfiability solving.

Related papers

• Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints [0.0]
  We introduce and benchmark a local search for the NP-complete satisfiability problem 3-SAT.<n>Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima.<n>We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N=15000.
  arXiv  Detail & Related papers  (2025-06-18T18:00:01Z)
• Bayesian Optimization with Inexact Acquisition: Is Random Grid Search Sufficient? [12.182108642150103]
  We show that inexact BO algorithms can still achieve sublinear cumulative regret.<n>Motivated by such findings, we provide both theoretical justification and numerical validation for random grid search.
  arXiv  Detail & Related papers  (2025-06-13T14:35:39Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  We propose a resource-constrained for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. We demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks.
  arXiv  Detail & Related papers  (2024-10-11T18:20:08Z)
• Stochastic Zeroth-Order Optimization under Strongly Convexity and Lipschitz Hessian: Minimax Sample Complexity [59.75300530380427]
  We consider the problem of optimizing second-order smooth and strongly convex functions where the algorithm is only accessible to noisy evaluations of the objective function it queries. We provide the first tight characterization for the rate of the minimax simple regret by developing matching upper and lower bounds.
  arXiv  Detail & Related papers  (2024-06-28T02:56:22Z)
• qPOTS: Efficient batch multiobjective Bayesian optimization via Pareto optimal Thompson sampling [0.0]
  A sample-efficient approach to solving multiobjective optimization is via process oracle (GP) surrogates and MOBOOTS$.<n>We propose a Thompson sampling (TS) based approach ($qtextttPOTS$)<n>$qtextttPOTS$ solves a cheap multiobjective optimization on the GP posteriors with evolutionary approaches.
  arXiv  Detail & Related papers  (2023-10-24T12:35:15Z)
• Landscape Surrogate: Learning Decision Losses for Mathematical Optimization Under Partial Information [48.784330281177446]
  Recent works in learning-integrated optimization have shown promise in settings where the optimization is only partially observed or where general-purposes perform poorly without expert tuning. We propose using a smooth and learnable Landscape Surrogate as a replacement for $fcirc mathbfg$. This surrogate, learnable by neural networks, can be computed faster than the $mathbfg$ solver, provides dense and smooth gradients during training, can generalize to unseen optimization problems, and is efficiently learned via alternating optimization.
  arXiv  Detail & Related papers  (2023-07-18T04:29:16Z)
• An Algorithm with Optimal Dimension-Dependence for Zero-Order Nonsmooth Nonconvex Stochastic Optimization [37.300102993926046]
  We study the complexity of producing neither smooth nor convex points of Lipschitz objectives which are possibly using only zero-order evaluations. Our analysis is based on a simple yet powerful. Goldstein-subdifferential set, which allows recent advancements in. nonsmooth non optimization.
  arXiv  Detail & Related papers  (2023-07-10T11:56:04Z)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  We propose a novel method named Multi-block-probe Variance Reduced (MSVR) to alleviate the complexity of compositional problems. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on strongity.
  arXiv  Detail & Related papers  (2022-07-18T12:03:26Z)
• An Efficient Batch Constrained Bayesian Optimization Approach for Analog Circuit Synthesis via Multi-objective Acquisition Ensemble [11.64233949999656]
  We propose an efficient parallelizable Bayesian optimization algorithm via Multi-objective ACquisition function Ensemble (MACE) Our proposed algorithm can reduce the overall simulation time by up to 74 times compared to differential evolution (DE) for the unconstrained optimization problem when the batch size is 15. For the constrained optimization problem, our proposed algorithm can speed up the optimization process by up to 15 times compared to the weighted expected improvement based Bayesian optimization (WEIBO) approach, when the batch size is 15.
  arXiv  Detail & Related papers  (2021-06-28T13:21:28Z)
• A Momentum-Assisted Single-Timescale Stochastic Approximation Algorithm for Bilevel Optimization [112.59170319105971]
  We propose a new algorithm -- the Momentum- Single-timescale Approximation (MSTSA) -- for tackling problems. MSTSA allows us to control the error in iterations due to inaccurate solution to the lower level subproblem.
  arXiv  Detail & Related papers  (2021-02-15T07:10:33Z)
• Convergence of adaptive algorithms for weakly convex constrained optimization [59.36386973876765]
  We prove the $mathcaltilde O(t-1/4)$ rate of convergence for the norm of the gradient of Moreau envelope. Our analysis works with mini-batch size of $1$, constant first and second order moment parameters, and possibly smooth optimization domains.
  arXiv  Detail & Related papers  (2020-06-11T17:43:19Z)
• Self-Directed Online Machine Learning for Topology Optimization [58.920693413667216]
  Self-directed Online Learning Optimization integrates Deep Neural Network (DNN) with Finite Element Method (FEM) calculations. Our algorithm was tested by four types of problems including compliance minimization, fluid-structure optimization, heat transfer enhancement and truss optimization. It reduced the computational time by 2 5 orders of magnitude compared with directly using methods, and outperformed all state-of-the-art algorithms tested in our experiments.
  arXiv  Detail & Related papers  (2020-02-04T20:00:28Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.