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

Researchers have introduced AFSAT, a GPU-accelerated pseudo-Boolean solver based on continuous local search. By leveraging the JAX compiler, AFSAT overcomes memory and floating-point limitations, delivering superior performance and near-linear scaling across multiple accelerators.

Computer Science > Artificial Intelligence

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

View PDF HTML (experimental)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.

Bibliographic and Citation Tools

Code, Data and Media Associated with this Article

Demos

Recommenders and Search Tools

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

Source: arXiv cs.AI Recent

More in this category

agentic-systems

Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Researchers have introduced Lean4Agent, the first framework that leverages the Lean4 formal language to model and verify AI agent workflows. By addressing natural language ambiguity, it significantly enhances the reliability and execution performance of LLMs.

agentic-systems

CrowdMath: A Dataset of Crowdsourced Mathematical Research Discussions

The newly introduced CrowdMath dataset evaluates AI's ability in collaborative mathematical problem-solving. While frontier LLMs excel at individual reasoning, they struggle to understand the functional roles of contributions in collaborative research discussions.

agentic-systems

Exploring Agentic Tool-Calling Decisions via Uncertainty-Aligned Reinforcement Learning

Researchers have proposed TRUST, a novel reinforcement learning framework that aligns uncertainty quantification with reward design to improve tool-calling decisions in LLM agents, preventing overconfident mistakes.

agentic-systems

Detecting and Mitigating Bias by Treating Fairness as a Symmetry Operation

Researchers propose a novel framework that treats fairness in machine learning as a symmetry operation, mitigating bias by over 90% with minimal impact on accuracy.

agentic-systems

A Study of Parallel Continuous Local Search

A new study explores parallel Continuous Local Search (CLS) as an efficient approach for solving Boolean satisfiability (SAT) problems, offering key insights for implementation on modern accelerator hardware.

agentic-systems

CARVE-Q: Quantum-Proposed, Classically Certified Interactive Driving Repair

Researchers have introduced CARVE-Q, a breakthrough architecture combining quantum search with classical verification to solve interactive driving repair for autonomous vehicles. This system enables autonomous vehicles to make rapid emergency maneuver repairs using quantum algorithms while ensuring absolute safety through classical verification certificates.

EXPLORE TOPICS