A dynamic SAT solver based on digital memcomputing machines (DMMs), written in Rust.
SpinSAT solves Boolean satisfiability (SAT) problems by mapping them onto a system of coupled ordinary differential equations (ODEs). Instead of discrete search (DPLL/CDCL), it uses continuous-time dynamics where Boolean variables become voltages and memory variables guide the system toward satisfying assignments.
The approach is based on the research paper:
S.R.B. Bearden, Y.R. Pei, M. Di Ventra. "Efficient Solution of Boolean Satisfiability Problems with Digital MemComputing." Scientific Reports 10, 19741 (2020). https://doi.org/10.1038/s41598-020-76666-2
Key results from the paper:
- Power-law scaling of integration steps for hard planted-solution 3-SAT instances (CDC class), compared to exponential scaling for WalkSAT and SID
- No chaotic dynamics — the system avoids exponential energy growth, unlike previous dynamical approaches
- Collective variable updates — long-range order enables the system to explore the solution space efficiently
- Successfully solved all tested competition instances from the 2017 and 2018 SAT Competition Random Tracks within the 5000-second timeout
SpinSAT targets the Experimental Track of the International SAT Competition 2026. This track is designed for solvers using unconventional techniques not yet supported by certificate generation — a natural fit for a physics-inspired ODE solver.
- Track: Experimental (no UNSAT proof certificates required)
- Timeout: 5000 seconds per instance
- Environment: Ubuntu 24.04, Intel Xeon Platinum 8368, 32 GB RAM, single-threaded
- Solver type: Hybrid DMM-CaDiCaL (ODE solver for SAT + CDCL fallback for UNSAT detection)
- April 19, 2026: Solver registration + benchmark submission
- April 26, 2026: Solver code submission
- May 17, 2026: System description document
- Parse a SAT instance in DIMACS CNF format into a polarity matrix
Q - Preprocess with a 6-technique CNF simplification pipeline (unit propagation, pure literal elimination, subsumption, self-subsuming resolution, BVE, failed literal probing)
- Initialize continuous voltages
v_n ∈ [-1, 1]and memory variablesx_{s,m},x_{l,m} - Integrate the DMM equations of motion using forward-Euler, RK4, or Trapezoid with adaptive time step
- Check if all clause constraints
C_m < 1/2— if so, threshold voltages to obtain a Boolean assignment - Restart with cycling or cold restart strategies when the solver stagnates
SpinSAT includes a bidirectional integration with CaDiCaL, a state-of-the-art CDCL solver, for UNSAT detection:
- Signal detection — monitors DMM integration for stagnation patterns (unsat count plateaus, memory saturation) that suggest the instance may be unsatisfiable
- Mid-solve handoff — when stagnation is detected, DMM's best voltages seed CaDiCaL's phase hints and frustrated variables (highest x_l) become CaDiCaL assumptions
- Bounded CDCL attempt — CaDiCaL runs with a conflict budget; if it proves UNSAT, we're done; if inconclusive, its learned information feeds back to DMM
- Final fallback — after DMM timeout, CaDiCaL gets all remaining time with DMM-informed phase hints
This hybrid approach means SpinSAT can solve SAT instances via ODE integration (its strength) while detecting UNSAT instances via CaDiCaL — without paying overhead on satisfiable instances.
Requires Rust toolchain (1.75+):
cargo build --releaseFor the competition, a pre-compiled static Linux binary is included for environments without Rust.
./target/release/spinsat <instance.cnf>Output follows the SAT competition standard format:
s SATISFIABLE
v 1 -2 3 -4 5 0
Results tracked in a SQLite database (benchmarks.db) with full reproducibility metadata. Run official benchmarks with:
# Initialize the benchmark database (one-time setup)
python3 scripts/init_benchmarks_db.py
# Run an official recorded benchmark
python3 scripts/benchmark_suite.py --suite large --record --tag v0.4.0
# Compare results across versions
python3 scripts/compare_results.py --by-size- Dashboard — interactive benchmark visualization (PAR-2 trends, version comparison, SQL explorer)
- Download
benchmarks.dbfrom Releases for local analysis with any SQLite client
| Suite | Vars | SpinSAT Solved | SpinSAT PAR-2 | Kissat PAR-2 |
|---|---|---|---|---|
| Small | 100-250 | 40/40 | 2.4 | 1.3 |
| Medium | 250-500 | 40/40 | 60 | 11 |
| Large | 500-2000 | 26/26 | 429 | 64 |
| Phase | Large PAR-2 | Solved | Key Change |
|---|---|---|---|
| Phase 1 (baseline) | 2113 | 24/26 | Core Euler solver |
| Phase 3 (heuristics) | 608 | 26/26 | Restarts + per-clause α_m |
| Phase 4 (optimized) | 429 | 26/26 | Auto-zeta + single-pass derivatives |
- Register at organizers@satcompetition.org (deadline: April 19, 2026)
- Submit 20 benchmark instances (deadline: April 19, 2026)
- Verify no instance solvable by MiniSat in under 60s (competition requirement)
- Verify all solvable by SpinSAT within 1 hour
- Final solver code submission (deadline: April 26, 2026)
- System description document, 1-2 pages, IEEE Proceedings style PDF (deadline: May 17, 2026)
- Test solver in competition Docker image (
registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:latest) - Make repository public after submission deadline
Versioning is fully automated via release-plz. No conventional commits required.
- Push to
main→ Release PR auto-created with version bump + CHANGELOG - Merge the Release PR → git tag + GitHub Release + crates.io publish
- Pre-compiled static Linux binary (
x86_64-unknown-linux-musl) attached to every release
# Install from crates.io
cargo install spinsat
# Or download the binary from GitHub Releases
gh release download --pattern 'spinsat' --repo seanbearden/SpinSAT| Tool | Version | Purpose |
|---|---|---|
| Rust (rustc) | 1.94.0 | Solver implementation language |
| release-plz | latest | Automated versioning, CHANGELOG, crates.io publish |
| CaDiCaL | 2.1.3 | CDCL solver for hybrid UNSAT detection (linked via FFI) |
| Kissat | 4.0.4 | CDCL baseline solver for comparison |
| MiniSat | 2.2.1 | Benchmark difficulty validation |
| gratchk | (MLton build) | Competition-grade SAT certificate verifier |
| check_sat | (custom C) | Fast local solution verifier |
| gtimeout | (coreutils) | macOS timeout command |
SpinSAT is developed with Claude Code (Anthropic's AI coding agent) and Gas Town, a multi-agent workspace manager. Gas Town coordinates persistent crew agents and transient polecat workers across rigs, using automated issue tracking, merge queues, and inter-agent communication to maintain development velocity.
- Main paper (open access)
- Supplementary materials (linked from main paper)
- SAT Competition 2026