ashen-navigator/neurosat-solver

🧠 NeuroSAT Solver: GPU-Accelerated Neural SAT Solving

A fast, GPU-accelerated SAT solver guided by neural networks, combining three paradigms:

1. Differentiable GPU Optimization (GaloisSAT/TurboSAT-style) — reformulates SAT as continuous optimization via finite-field algebra, enabling massive parallelism on GPU
2. GNN-based Variable Phase Prediction (NeuroBack-style) — message-passing neural network predicts variable assignments to warm-start the solver
3. CDCL Completeness (CaDiCaL via PySAT) — guarantees correct SAT/UNSAT answers with neural warm-starting

Architecture

                    ┌─────────────────────────┐
                    │   Input: CNF Formula     │
                    │   (DIMACS format)        │
                    └──────────┬──────────────┘
                               │
                    ┌──────────▼──────────────┐
                    │  Phase 1: GNN Guidance   │
                    │  (if model available)    │
                    │  • Variable phases       │
                    │  • Activity scores       │
                    │  • ~1-2s inference        │
                    └──────────┬──────────────┘
                               │
                    ┌──────────▼──────────────┐
                    │  Phase 2: GPU Solver     │
                    │  • N parallel candidates │
                    │  • Adam + finite-field   │
                    │  • Sparse matmul on GPU  │
                    │  • Extract partial soln  │
                    └──────────┬──────────────┘
                               │
                    ┌──────────▼──────────────┐
                    │  Phase 3: CDCL Solver    │
                    │  • CaDiCaL backend       │
                    │  • Warm-started with     │
                    │    GPU partial + GNN     │
                    │    phase predictions     │
                    │  • Complete & correct    │
                    └──────────┬──────────────┘
                               │
                    ┌──────────▼──────────────┐
                    │  Output: SAT/UNSAT      │
                    │  + satisfying assignment │
                    └─────────────────────────┘

Key Innovation: Differentiable SAT on GPU

Based on GaloisSAT (8.4× speedup over Kissat) and TurboSAT (27× over CaDiCaL):

# Boolean algebra → finite-field arithmetic:
#   NOT x  = 1 - x
#   x OR y = x + y - x*y  
#   x AND y = x * y

# Clause satisfaction (differentiable):
# C_sat = 1 - ∏(1 - literal_i)

# N candidate assignments optimized in parallel via Adam:
logits = torch.randn(N, n_vars, requires_grad=True)
optimizer = torch.optim.Adam([logits], lr=0.5)

# One matmul evaluates ALL candidates on ALL clauses simultaneously

Installation

pip install torch numpy python-sat
git clone https://huggingface.co/ashen-navigator/neurosat-solver
cd neurosat-solver
pip install -e .

Quick Start

from neurosat_solver import HybridSATSolver, generate_random_3sat

# Generate a random 3-SAT instance
formula = generate_random_3sat(n_vars=100, clause_ratio=4.26)

# Solve with the hybrid neural solver
solver = HybridSATSolver()
result = solver.solve(formula, timeout=60.0)

print(f"Satisfiable: {result['satisfiable']}")
if result['satisfiable']:
    print(f"Verified: {formula.verify_assignment(result['assignment'])}")

Solve from DIMACS format

from neurosat_solver import HybridSATSolver

dimacs = """
p cnf 3 3
1 -2 3 0
-1 2 -3 0
1 2 3 0
"""

solver = HybridSATSolver()
result = solver.solve(dimacs)

Use individual components

from neurosat_solver import DifferentiableSATSolver, SolverConfig

# GPU solver only (no CDCL fallback)
config = SolverConfig(
    n_candidates=1024,     # Parallel candidates
    learning_rate=0.5,     # Aggressive learning rate
    max_iterations=2000,   # Max optimization steps
    n_restarts=5,          # Random restart rounds
)
gpu_solver = DifferentiableSATSolver(config)
result = gpu_solver.solve(formula, timeout=30.0)

Train a GNN guide

from neurosat_solver.train_gnn import train_gnn_guide

guide = train_gnn_guide(
    n_instances=5000,
    min_vars=10,
    max_vars=100,
    hidden_dim=128,
    n_mp_layers=6,
    n_epochs_pretrain=40,
    n_epochs_finetune=20,
    save_path="gnn_guide.pt",
)

# Use with hybrid solver
solver = HybridSATSolver(gnn_guide=guide)
result = solver.solve(formula)

Benchmark Results

On CPU (benchmarked on random 3-SAT instances):

Size (vars)	Mean Time	Solved
10	0.02s	3/3
20	0.08s	3/3
50	0.81s	3/3
100	14.3s	3/3

On GPU, the differentiable solver provides massive speedup via parallel candidate evaluation. The sparse clause-literal matmul scales efficiently to problems with millions of variables (see TurboSAT: 27× speedup on 1M+ variable problems).

Components

Component	File	Description
CNFFormula	cnf_parser.py	CNF representation, DIMACS parser, generators
DifferentiableSATSolver	gpu_solver.py	GPU differentiable optimization engine
SATGraphNet	gnn_guide.py	GNN for variable phase/activity prediction
CDCLSolver	cdcl_solver.py	CaDiCaL-backed CDCL with neural warm-start
HybridSATSolver	hybrid_solver.py	Full pipeline combining all components

GNN Architecture (NeuroBack-style)

The GNN operates on a bipartite variable-clause graph:

• Variable nodes: degree-based features
• Clause nodes: length-based features
• Meta node: reduces graph diameter from O(n) to 4
• Message passing: 6 layers with GRU updates + polarity-aware edges
• Self-attention: global context over variable embeddings
• Output: phase logits + activity scores per variable

Research References

• GaloisSAT — Differentiable Boolean Satisfiability via Finite Field Algebra (arxiv:2603.28796). 8.4× PAR-2 speedup on SAT Competition 2024.
• TurboSAT — Gradient-Guided Boolean Satisfiability on GPU-CPU Hybrid (arxiv:2511.07737). 27× average speedup over CaDiCaL on SAT Competition 2024.
• NeuroBack — Improving CDCL SAT Solving using Graph Neural Networks (arxiv:2110.14053). +5.2% problems solved on SATCOMP-2022.
• NeuroCore — Guiding High-Performance SAT Solvers with Unsat-Core Predictions (arxiv:1903.04671). +10% problems via GNN activity injection.
• ImitSAT — Boolean Satisfiability via Imitation Learning (arxiv:2509.25411). Perceiver-AR for learned branching.

GPU Acceleration

When a CUDA GPU is available, the differentiable solver automatically uses it:

config = SolverConfig(
    device="cuda",           # Use GPU
    n_candidates=4096,       # More candidates = more parallelism
    dtype="float16",         # Half precision for faster matmul
)
solver = DifferentiableSATSolver(config)

Key GPU optimizations:

• Sparse CSR matmul: Clause-literal matrix stored in sparse format → cuSPARSE GEMM
• Batch candidate evaluation: N assignments evaluated in one matmul
• Per-variable normalization: Information sharing across candidates (TurboSAT technique)
• Periodic LR restarts: Escape local minima (reset every 360 steps)

License

Apache 2.0