Research map / Architectures and efficiency / RNNs and normalization
Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes FastFourierSAT, a GPU-parallel hybrid SAT solver that computes CLS gradients via an FFT-based convolution for elementary symmetric polynomials, plus ERWA weighting and rephasing restarts.
Problem
Continuous local search (CLS) SAT solvers such as FourierSAT and GradSAT have slow, sequential gradient computation for hybrid (non-CNF) constraints, limiting their scalability and parallelism on hardware such as GPUs.
Approach
Compute the Walsh expansion of symmetric Boolean constraints via FFT-based convolution of elementary symmetric polynomials, turning evaluation into a vectorized trace whose reverse traversal yields gradients in O(k^2) work with O*(log k) ideal parallel time, mapped onto GPU threads, warps and SMs; adds ERWA-based constraint reweighting and rephasing restarts.
Key results
- FastFourierSAT computes gradients 31.36x faster on xor3 and 148.59x faster on card3 than CPU CLS prototypes.
- On weighted Max-Cut planted partition instances, FastFourierSAT finds the best solution for 323 instances versus 83 for the virtual best solver without CLS.
- On random cardinality benchmarks FastFourierSAT solves all instances, while GradSAT solves 478 vs 434 for the virtual best solver without CLS.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use GPU-parallel FastFourierSAT instead of previous CPU CLS implementations | gradient computation on xor3 · xor3 | gradient computation speedup: 31.36× | Helped |
| use GPU-parallel FastFourierSAT instead of previous CPU CLS implementations | gradient computation on card3 · card3 | gradient computation speedup: 148.59× | Helped |
| use FastFourierSAT instead of VBS w/o CLS | weighted Max-Cut · Weighted Max-Cut, 16, 16 | average score (%): 99.94 -> 100.00 | Helped |
| use FastFourierSAT instead of VBS w/o CLS | weighted Max-Cut · Weighted Max-Cut, 16, 32 | average score (%): 99.23 -> 99.90 | Helped |
| use FastFourierSAT instead of VBS w/o CLS | weighted Max-Cut · Weighted Max-Cut, 32, 16 | average score (%): 99.15 -> 99.96 | Helped |
| use FastFourierSAT instead of VBS w/o CLS | weighted Max-Cut · Weighted Max-Cut, 32, 32 | average score (%): 99.43 -> 99.71 | Helped |
| add restart heuristics (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=150 | average iterations (Par 2): 74.03 -> 21.03 | Helped |
| add restart heuristics (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=150 | instances solved: 98 -> 100 | Helped |
| run heuristic and no-heuristic strategies as a portfolio (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=200 | average iterations (Par 2): 405.8 -> 322.4 | Helped |
| run heuristic and no-heuristic strategies as a portfolio (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=200 | instances solved: 85 -> 89 | Helped |
| add restart heuristics (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=100 | average iterations (Par 2): 2.01 -> 2.2 | Hurt |
| add restart heuristics (ablation) | FastFourierSAT · Weighted 3-SAT SATLIB, n=250 | average iterations (Par 2): 1075 -> 797.8 | Helped |
Surprising findings
- On the parity learning benchmark, GradSAT solves fewer instances (300) than the virtual best solver without CLS (438), since that problem class is easier for CDCL and local search.
Limitations
- High bit precision is needed to control numerical round-off, raising computation and memory overhead.
- Preprocessing overhead for large instances and limited solving on some benchmarks versus CDCL and local search solvers.
Experimental setup
Datasets: SATLIB random cardinality formulas random XOR formulas parity learning with error instances planted partition weighted Max-Cut graphs
Benchmarks: SATLIB 3-SAT random cardinality benchmark parity learning with error benchmark weighted Max-Cut (MSE19 and planted partition)
Metrics: gradient computation time number of instances solved average score on Max-Cut number of best solutions average iterations (PAR-2)
Baselines: FourierSAT GradSAT NuWLS NuWLS-c SATLike SATLike-ck TT-Open-WBO PalSAT
Builds on: FourierSAT GradSAT ERWA projected gradient descent
Closest papers by meaning
- DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem (AAAI 2025 · similarity 0.86)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.83)
- Learning How to Cube (NeurIPS 2026 · similarity 0.82)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.82)
- HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation (NeurIPS 2024 · similarity 0.82)
- NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks (ICLR 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.