FFSAT is a native pseudo-Boolean (PB) Continuous Local Search (CLS) Satisfiability (SAT) solver that leverages recent developments in closed-form transformations of various pseudo-Boolean constraint types into continuous multilinear polynomial on a one-to-one basis.
The approach takes advantage of the JAX ecosystem, a modern high performance scientific computing framework, leveraging automatic differentiation and efficient optimization for fast distributed GPU kernels.
This work is based on recent theoretical advances by Kyrillidis et al1 and a proof-of-concept demonstration by Cen et al2. The code presented here is an implementation from scratch, and supports arbitrary PB-SAT problems that can be expressed in any combination of the constraint types enumerated below.
A note on naming convention: This does not use fast Fourier algorithm. The underlying transform is a Fourier transform, hence Fourier SAT. After this transform, this solver utilises a second discrete Fourier transform for fast polynomial evaluation on GPU, from which the fast is derived.
- Python >=3.10+ (TBD: Backward compatability to 3.8)
- For JAX acceleration with NVIDIA:
- CUDA >=12.1
- CUDNN >=9.1, <10.0
- NCCL >=2.18
- NVIDIA Driver >=525.60.13
- See JAX Installation for more details, or CPU/TPU requirements (untested).
Optionally, see https://github.com/NVIDIA/JAX-Toolbox for Docker images that may work.
-
Clone the repository:
git clone https://github.com/cjchristopher/ffsat.git cd ffsat -
Create and activate a virtual environment (recommended, your choice of environment management, venv here for illustration):
python -m venv venv source venv/bin/activate # On Windows: venv\Scripts\activate
-
Install JAX
See JAX Installation for instructions.
-
Install dependencies:
pip install -r requirements.txt
Core dependencies (see requirements.txt for complete list with versions):
- JAX (0.6.0) and JAX CUDA plugins
- jaxopt (0.8.5) - Optimization library
- NumPy (2.2.5)
- SciPy (1.15.2)
- tqdm (4.67.1) - Progress bars
- python-sat (1.8.dev16) - SAT utilities
- Rich (14.0.0) - Terminal formatting
- NVIDIA CUDA libraries (CUDA 12.x compatible)
All dependencies can be installed via:
pip install -r requirements.txtThe solver accepts files in standard DIMACS CNF format as well as an extended hybrid format that supports various constraint types.
- Comment lines starting with 'c' or '*'
- A problem line starting with 'p cnf' followed by the number of variables and clauses
- Clauses represented as space-separated integers ending with '0'
- Positive integers represent positive literals, negative integers represent negative literals
- Example:
1 -2 3 0represents (x₁ ∨ ¬x₂ ∨ x₃)
This solver extends the DIMACS format to support various constraint types using the following syntax:
-
Constraint lines either:
- Start with
h(hybrid marker), e.g.,h 1 2 0 - Start with constraint type directly, e.g.,
xor 1 2 0 - For standard CNF clauses, no prefix is needed, e.g.,
1 2 0
- Start with
-
Supported constraint types:
-
CNF clauses: Standard disjunction of literals
1 -2 3 0orh 1 -2 3 0 -
XOR constraints: Exactly one variable must be true
xor 1 2 3 0orh x 1 2 3 0orx 1 2 3 0 -
NAE (Not-All-Equal) constraints: Not all literals can have the same value
nae 1 2 3 0orh n 1 2 3 0orn 1 2 3 0 -
EO (Exactly-One) constraints: Exactly one literal must be true
eo 1 2 3 0orh e 1 2 3 0ore 1 2 3 0 -
AMO (At-Most-One) constraints: At most one literal can be true
amo 1 2 3 0orh a 1 2 3 0ora 1 2 3 0 -
Ek (Exactly-k) constraints: Exactly k literals must be true
ek <k> <literals> 0orh k <k> <literals> 0ork <k> <literals> 0Where
<k>is a non-zero positive integer:ek 2 1 2 3 0(at least 2 variables must be true)ek 4 1 2 3 4 5 6 0(more than 2 variables must be true)
-
Cardinality constraints: Specify how many literals in a set must be true
card <k> <literals> 0orh d <k> <literals> 0ord <k> <literals> 0Where
<k>can be:- A simple integer:
card 2 1 2 3 0(at least 2 of the variables must be true) - A negative integer:
card -2 1 2 3 0(fewer than 2 variables must be true) - With inequality prefix:
card >=2 1 2 3 0(at least 2 variables must be true)card >2 1 2 3 0(more than 2 variables must be true)card <2 1 2 3 0(fewer than 2 variables must be true)card <=2 1 2 3 0(at most 2 variables must be true)
- A simple integer:
-
The parser is flexible with shorthand notations for constraint types, allowing for both single-character identifiers (x, n, e, a, d, k) and full names (xor, nae, eo, amo, card, ek).
Run the solver with:
python ffsat.py [options] input_file.cnf-t, --timeout INT: Maximum runtime in seconds (default: 300)-b, --batch INT: Batch size per GPU (default: -1 = compute heuristic maximum)-r, --restart_thresh INT: Number of batches before reweighting (default: 0, never reweight)-f, --fuzz INT: Number of times to attempt fuzzing per batch (default: 0)-n, --n_devices INT: Number of devices (e.g., GPUs) to use (default: all available, 0 = use all)-i, --iters_desc INT: Descent iteration depth (default: 100)-d, --debug LEVEL: Set logging level: DEBUG, INFO, WARNING, or ERROR (default: ERROR)-e, --benchmark: Enable benchmark mode (reduces output verbosity)-c, --counting INT: Counting mode - count solutions until timeout (default: 0, disabled)-w, --warmup: Perform a warmup run before starting the timer (may improve performance with JAX compilation cache)-s, --rand_seed: Randomize the random seed (default: uses fixed seed for reproducibility)-p, --prefix FILE: Path to file containing fixed variable assignments (one assignment per line, using SAT solver output format with negated literals)-y, --profile: Enable profiling (saves JAX trace to/tmp/jax-traceand device memory profile tomemory.prof)
Basic usage:
python ffsat.py problem.cnfRunning with a 10-minute timeout and specific batch size:
python ffsat.py problem.cnf -t 600 -b 32Enable five fuzzing passes per batch:
python ffsat.py problem.cnf -f 5Run with debugging enabled and profiling:
python ffsat.py problem.cnf -d DEBUG -pUse a prefix file with fixed variable assignments:
python ffsat.py problem.cnf -p prefix.txtUse specific number of GPUs with custom iteration depth:
python ffsat.py problem.cnf -n 2 -i 200Counting mode - find all solutions within 5 minutes:
python ffsat.py problem.cnf -t 300 -c 1The solver outputs:
- Progress information during the search
- SAT/UNSAT result
- Variable assignments for satisfiable instances in DIMACS format (lines starting with "v")
- Timing and performance statistics
The solver uses JAX for hardware acceleration and automatic differentiation. It transforms boolean satisfiability constraints into continuous functions that can be minimized using gradient-based methods.
FFSAT supports multiple optimization backends (default: pgd):
- pgd: Projected Gradient Descent with box constraints (JAXOPT)
- lbfgsb: Limited-memory BFGS with bounds (JAXOPT)
- josp-lbfgsb: JAXOPT's Scipy-wrapped L-BFGS-B
- sp-lbfgsb: Scipy L-BFGS-B with JAX compiled objective function
Note: The solver algorithm is currently hardcoded in the source. Support for command-line selection may be added in future versions.
Dual-licensed under:
- Apache License 2.0 (
Apache-2.0) - GNU General Public License v2.0 or later (
GPL-2.0-or-later)
You may choose either license when using, modifying, or redistributing this project.
Source files use the combined SPDX expression:
SPDX-License-Identifier: Apache-2.0 OR GPL-2.0-or-later
License texts: see LICENSE-APACHE (Apache 2.0) and LICENSE (GPL v2).
Contributions are accepted under the same dual-license terms.
Footnotes
-
Kyrillidis, A., Shrivastava, A., Vardi, M. Y., & Zhang, Z. (2021). Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions. Artificial Intelligence, 299, 103559.
↩
-
Cen, Y., Zhang, Z., & Fong, X. (2025). Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs. Proceedings of the AAAI Conference on Artificial Intelligence, 39(11), 11140-11149.
↩
