Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver

• URL: http://arxiv.org/abs/2606.06641v1
• Date: Thu, 04 Jun 2026 18:47:45 GMT
• Title: Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver
• Abstract summary: We present AFSAT, a GPU-accelerated solver for pseudo-Boolean satisfiability based on continuous local search.<n>We demonstrate substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept.<n>We achieve near-linear throughput when scaling to multiple accelerators via JAX sharding.
• Score: 0.6353525052246608
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present Accelerated Fourier SAT (AFSAT), a GPU-accelerated solver for pseudo-Boolean satisfiability based on continuous local search (CLS). AFSAT realises the proof-of-concept approach, FastFourierSAT, into a fully-engineered solver supporting any heterogeneous mixture of symmetric constraint types and lengths within a single problem instance. Using the JAX compiler, AFSAT leverages pure function composition, automatic vectorisation, automatic differentiation, and just-in-time (JIT) compilation to perform massively parallel CLS across batches of candidate assignments. We demonstrate substantially improved numerical stability, runtime performance, and memory efficiency over the proof-of-concept. We achieve this by way of identifying and addressing various limitations that arise from memory latency and floating-point representation, as well as leveraging automatic parallelisation and compact representations. The inherent representational and stability limitations of floating point are partially addressed by a tailored discrete Fourier transform implementation. We achieve near-linear throughput when scaling to multiple accelerators via JAX array sharding.

Related papers

• Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
  We present an exact and tractable algorithm for sampling from the constrained mean-field posterior under any constraint expressible as a finite automaton.<n>The approach guarantees constraint satisfaction by construction, supports both greedy and sampling-based decoding, and is compatible with parallel and block-wise decoding.<n> Empirical evaluations on Dream-7B and LLaDA-8 show substantial accuracy gains across various tasks.
  arXiv  Detail & Related papers  (2026-07-08T05:48:57Z)
• TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System [7.530665570222049]
  State-of-the-art satisfiability solvers rely heavily on inherently sequential conflict-driven search algorithms.<n>Inspired by neural network training, we formulate the SAT problem as a binarized matrix-matrix multiplication layer.<n>We combine the strengths of parallel differentiable optimization and sequential search to accelerate SAT on a hybrid GPU- CPU system.
  arXiv  Detail & Related papers  (2025-11-11T01:41:40Z)
• Orthogonal Finetuning Made Scalable [92.34573849209238]
  Orthogonal finetuning (OFT) offers highly parameter-efficient adaptation while preventing catastrophic forgetting, but its high runtime and memory demands limit practical deployment.<n>We identify the core computational bottleneck in OFT as its weight-centric implementation, which relies on costly matrix-matrix multiplications with cubic complexity.<n>We propose OFTv2, an input-centric reformulation that instead uses matrix-vector multiplications (i.e., matrix-free computation), reducing the computational cost to quadratic.<n>These modifications allow OFTv2 to achieve up to 10x faster training and 3x lower GPU memory usage without
  arXiv  Detail & Related papers  (2025-06-24T17:59:49Z)
• High-Throughput SAT Sampling [3.8108678341258138]
  We present a novel technique for GPU-accelerated satisfiability (SAT) sampling.<n>Our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions.<n>We achieve GPU-accelerated sampling with significant improvements ranging from $33.6times$ to $523.6times$ over state-of-the-art samplers.
  arXiv  Detail & Related papers  (2025-02-12T03:20:45Z)
• Sparsity-Constraint Optimization via Splicing Iteration [1.3622424109977902]
  We develop an algorithm named Sparsity-Constraint Optimization via sPlicing itEration (SCOPE) SCOPE converges effectively without tuning parameters. We apply SCOPE to solve quadratic optimization, learn sparse classifiers, and recover sparse Markov networks for binary variables. Our open-source Python package skscope based on C++ implementation is publicly available on GitHub.
  arXiv  Detail & Related papers  (2024-06-17T18:34:51Z)
• Equivariant Scalar Fields for Molecular Docking with Fast Fourier Transforms [11.163940886337798]
  We show how machine learning can learn a scoring function with a functional form that allows for more rapid optimization. We benchmark our scoring functions on two simplified docking-related tasks: decoy pose scoring and rigid conformer docking. Our method attains similar but faster performance on crystal structures compared to the widely-used Vina and Gnina scoring functions, and is more robust on predicted structures.
  arXiv  Detail & Related papers  (2023-12-07T14:32:32Z)
• Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs [5.245714076090567]
  We propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.
  arXiv  Detail & Related papers  (2023-08-29T04:50:07Z)
• Performance Embeddings: A Similarity-based Approach to Automatic Performance Optimization [71.69092462147292]
  Performance embeddings enable knowledge transfer of performance tuning between applications. We demonstrate this transfer tuning approach on case studies in deep neural networks, dense and sparse linear algebra compositions, and numerical weather prediction stencils.
  arXiv  Detail & Related papers  (2023-03-14T15:51:35Z)
• Multiway Non-rigid Point Cloud Registration via Learned Functional Map Synchronization [105.14877281665011]
  We present SyNoRiM, a novel way to register multiple non-rigid shapes by synchronizing the maps relating learned functions defined on the point clouds. We demonstrate via extensive experiments that our method achieves a state-of-the-art performance in registration accuracy.
  arXiv  Detail & Related papers  (2021-11-25T02:37:59Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Square Root Bundle Adjustment for Large-Scale Reconstruction [56.44094187152862]
  We propose a new formulation for the bundle adjustment problem which relies on nullspace marginalization of landmark variables by QR decomposition. Our approach, which we call square root bundle adjustment, is algebraically equivalent to the commonly used Schur complement trick. We show in real-world experiments with the BAL datasets that even in single precision the proposed solver achieves on average equally accurate solutions.
  arXiv  Detail & Related papers  (2021-03-02T16:26:20Z)

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.