# FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints

arXiv: https://arxiv.org/abs/1912.01032 · HTML: https://mlsanity.com/paper/1912.01032/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Dec 2019.

## Built on by (most cited first, 12 of 12)

- [Goal-Aware Neural SAT Solver](https://mlsanity.com/paper/2106.07162/) (2021)
- [Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs](https://mlsanity.com/paper/2308.15020/) (2023)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints](https://mlsanity.com/paper/2301.09833/) (2023)
- [Understanding GNNs for Boolean Satisfiability through Approximation Algorithms](https://mlsanity.com/paper/2408.15418/) (2024)
- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)
- [DPO: Dynamic-Programming Optimization on Hybrid Constraints](https://mlsanity.com/paper/2205.08632/) (2022)
- [TurboSAT: Gradient-Guided Boolean Satisfiability Accelerated on GPU-CPU Hybrid System](https://mlsanity.com/paper/2511.07737/) (2025)
- [Quantum-Inspired Approximations to Constraint Satisfaction Problems](https://mlsanity.com/paper/2212.04016/) (2022)
- [Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization](https://mlsanity.com/paper/2506.00674/) (2025)
- [FourierCSP: Differentiable Constraint Satisfaction Problem Solving by Walsh-Fourier Expansion](https://mlsanity.com/paper/2510.04480/) (2025)
- [GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra](https://mlsanity.com/paper/2603.28796/) (2026)

## Abstract (arXiv)

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side, especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers, has been remarkable. Yet, while SAT solvers aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF) have become quite mature, SAT solvers that are effective on other types of constraints, e.g., cardinality constraints and XORs, are less well studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time. To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.