Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic

• URL: http://arxiv.org/abs/2603.22877v1
• Date: Tue, 24 Mar 2026 07:22:30 GMT
• Title: Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
• Abstract summary: We introduce FourierSMT as a scalable and highly parallelizable continuous-variable optimization framework for satisfiability modulo theories.<n>The framework is benchmarked for large-scale scheduling and placement problems with up to 10,000 variables and 700,000 constraints, achieving 8-fold speedups.
• Score: 2.8037951156321377
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Efficient solutions for satisfiability modulo theories (SMT) are integral in industrial applications such as hardware verification and design automation. Existing approaches are predominantly based on conflict-driven clause learning, which is structurally difficult to parallelize and therefore scales poorly. In this work, we introduce FourierSMT as a scalable and highly parallelizable continuous-variable optimization framework for SMT. We generalize the Walsh-Fourier expansion (WFE), called extended WFE (xWFE), from the Boolean domain to a mixed Boolean-real domain, which allows the use of gradient methods for SMT. This addresses the challenge of finding satisfying variable assignments to high-arity constraints by local updates of discrete variables. To reduce the evaluation complexity of xWFE, we present the extended binary decision diagram (xBDD) and map the constraints from xWFE to xBDDs. We then show that sampling the circuit-output probability (COP) of xBDDs under randomized rounding is equivalent to the expectation value of the xWFEs. This allows for efficient computation of the constraints. We show that the reduced problem is guaranteed to converge and preserves satisfiability, ensuring the soundness of the solutions. The framework is benchmarked for large-scale scheduling and placement problems with up to 10,000 variables and 700,000 constraints, achieving 8-fold speedups compared to state-of-the-art SMT solvers. These results pave the way for GPU-based optimization of SMTs with continuous systems.

Related papers

• DRAFTO: Decoupled Reduced-space and Adaptive Feasibility-repair Trajectory Optimization for Robotic Manipulators [4.0407133618465005]
  This paper introduces a new algorithm for trajectory optimization, Decoupled Reduced-space and Adaptive Feasibility-repair Trajectory Optimization (DRAFTO)<n>To reduce the number of repeated constrained optimizations while handling joint-limit feasibility, the optimization is decoupled into a reduced-space Gauss-Newton (GN) descent.<n>The results of our benchmark tests against optimization-based planners, such as CHOMP, TrajOpt, GPMP2, and FACTO, validate the high efficiency and reliability across diverse scenarios and tasks.
  arXiv  Detail & Related papers  (2026-03-10T20:24:42Z)
• The Theory and Practice of MAP Inference over Non-Convex Constraints [11.058494098615576]
  In safety-critical settings, probabilistic ML systems have to make predictions subject to algebraic constraints.<n>This makes computing this constrained maximum a posteriori (MAP) prediction efficiently and reliably extremely challenging.<n>We devise a scalable message-passing algorithm for this tractable fragment.<n>Then, we devise a general constrained MAP strategy that interleaves partitioning the domain into convex feasible regions.
  arXiv  Detail & Related papers  (2026-02-09T14:05:58Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• PT$^2$-LLM: Post-Training Ternarization for Large Language Models [52.4629647715623]
  Large Language Models (LLMs) have shown impressive capabilities across diverse tasks, but their large memory and compute demands hinder deployment.<n>We propose PT$2$-LLM, a post-training ternarization framework tailored for LLMs.<n>At its core is an Asymmetric Ternary Quantizer equipped with a two-stage refinement pipeline.
  arXiv  Detail & Related papers  (2025-09-27T03:01:48Z)
• FMIP: Joint Continuous-Integer Flow For Mixed-Integer Linear Programming [52.52020895303244]
  Mixed-Integer Linear Programming (MILP) is a foundational tool for complex decision-making problems.<n>We propose Joint Continuous-Integer Flow for Mixed-Integer Linear Programming (FMIP), which is the first generative framework that models joint distribution of both integer and continuous variables for MILP solutions.<n>FMIP is fully compatible with arbitrary backbone networks and various downstream solvers, making it well-suited for a broad range of real-world MILP applications.
  arXiv  Detail & Related papers  (2025-07-31T10:03:30Z)
• Decentralized Nonconvex Composite Federated Learning with Gradient Tracking and Momentum [78.27945336558987]
  Decentralized server (DFL) eliminates reliance on client-client architecture.<n>Non-smooth regularization is often incorporated into machine learning tasks.<n>We propose a novel novel DNCFL algorithm to solve these problems.
  arXiv  Detail & Related papers  (2025-04-17T08:32:25Z)
• Optimizing LLM Inference: Fluid-Guided Online Scheduling with Memory Constraints [14.341123057506827]
  Large Language Models (LLMs) are indispensable in today's applications, but their inference procedure demands significant computational resources.<n>This paper formulates LLM inference optimization as a multi-stage online scheduling problem.<n>We develop a fluid dynamics approximation to provide a tractable benchmark that guides algorithm design.
  arXiv  Detail & Related papers  (2025-04-15T16:00:21Z)
• Taming Flow Matching with Unbalanced Optimal Transport into Fast Pansharpening [10.23957420290553]
  We propose the Optimal Transport Flow Matching framework to achieve one-step, high-quality pansharpening.<n>The OTFM framework enables simulation-free training and single-step inference while maintaining strict adherence to pansharpening constraints.
  arXiv  Detail & Related papers  (2025-03-19T08:10:49Z)
• Efficiently Training Deep-Learning Parametric Policies using Lagrangian Duality [55.06411438416805]
  Constrained Markov Decision Processes (CMDPs) are critical in many high-stakes applications.<n>This paper introduces a novel approach, Two-Stage Deep Decision Rules (TS- DDR) to efficiently train parametric actor policies.<n>It is shown to enhance solution quality and to reduce computation times by several orders of magnitude when compared to current state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-05-23T18:19:47Z)
• Distributed Extra-gradient with Optimal Complexity and Communication Guarantees [60.571030754252824]
  We consider monotone variational inequality (VI) problems in multi-GPU settings where multiple processors/workers/clients have access to local dual vectors. Extra-gradient, which is a de facto algorithm for monotone VI problems, has not been designed to be communication-efficient. We propose a quantized generalized extra-gradient (Q-GenX), which is an unbiased and adaptive compression method tailored to solve VIs.
  arXiv  Detail & Related papers  (2023-08-17T21:15:04Z)
• Stochastic Inexact Augmented Lagrangian Method for Nonconvex Expectation Constrained Optimization [88.0031283949404]
  Many real-world problems have complicated non functional constraints and use a large number of data points. Our proposed method outperforms an existing method with the previously best-known result.
  arXiv  Detail & Related papers  (2022-12-19T14:48:54Z)
• Federated Expectation Maximization with heterogeneity mitigation and variance reduction [0.0]
  This paper introduces FedEM, which is the first extension of the Expectation Maximization (EM) algorithm for latent variable models. To alleviate complexity of communication, FedEM appropriately defined complete data sufficient statistics. Results presented support our theoretical findings as well as an application handles missing values imputation for biodiversity monitoring.
  arXiv  Detail & Related papers  (2021-11-03T09:14:34Z)

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.