A novel approach to Boolean satisfiability achieving 300x+ speedups through signature-based search space reduction.
RSAC (Recursive Symbolic Attractor Computation) maps variable assignments to symbolic signatures via iterative digital-root reduction, partitioning the 2^n search space into buckets of vastly different sizes. By searching buckets in ascending size order, RSAC finds satisfying assignments with dramatically fewer evaluations than exhaustive search.
- 268.71x speedup on 16-variable planted solution (8330 → 31 checks)
- 227.89x speedup on 14-variable backdoor problem (2051 → 9 checks)
- 107.95x speedup on structured backdoor instances
- 64x speedup on 16-variable problems with preprocessing
- Consistent 100x+ improvements on structured instances
- 100% correctness verified across comprehensive test suite
| Variables | Avg BF Checks | Avg RSAC Checks | Avg Speedup |
|---|---|---|---|
| n=12 | 68.1 | 27.5 | 2.94x |
| n=14 | 823.1 | 54.6 | 10.34x |
| n=16 | 1129.3 | 85.4 | 47.16x |
| n=18 | 3301.6 | 228.2 | 38.0x |
| Problem Type | Best Speedup | Method | Instance |
|---|---|---|---|
| Planted Solution | 268.71x | Basic RSAC | 16v (8330→31) |
| Backdoor | 227.89x | Hybrid RSAC | 14v (2051→9) |
| Crafted Hard | 55.76x | Hybrid RSAC | 14v (6134→110) |
| Structured SAT | 21.56x | Hybrid RSAC | 14v (9379→435) |
git clone https://github.com/Betti-Labs/rsac-collapse-engine.git
cd rsac-collapse-engine
python -m venv venv
source venv/bin/activate # On Windows: venv\Scripts\activate
pip install -r requirements.txt# Run basic SAT benchmarks
python src/benchmarks.py --series sat --ns 12 14 16 --instances 10
# Run comprehensive stress test
python stress_test.py --all
# Test on SAT competition instances
python sat_competition_benchmarks.py --local-only
# Run ultimate benchmark suite
python ultimate_rsac_benchmark.pyrsac-collapse-engine/
├── src/rsac/ # Core RSAC implementation
│ ├── collapse.py # Signature generation algorithms
│ ├── sat.py # SAT utilities and generators
│ ├── bucket_search.py # Bucket search algorithms
│ ├── hybrid_solver.py # Advanced hybrid solver
│ ├── advanced_signatures.py # Multiple signature variants
│ └── utils.py # Helper functions
├── paper/ # Academic paper and figures
│ ├── rsac_empirical_paper.tex # LaTeX source
│ └── rsac_empirical_paper.pdf # Compiled paper
├── benchmarks/ # Benchmark scripts
│ ├── stress_test.py # Comprehensive testing
│ ├── sat_competition_benchmarks.py # Real-world instances
│ └── ultimate_rsac_benchmark.py # Advanced benchmarks
├── data/ # Results and analysis
├── requirements.txt # Python dependencies
└── LICENSE # Apache 2.0 License
- Signature Generation: Convert bit assignments to symbolic sequences using position-based encoding
- Recursive Reduction: Apply digital-root reduction iteratively to create signature layers
- Extended Signatures: Combine final layers with entropy information for robust clustering
- Bucket Creation: Group all 2^n assignments by signature into buckets of varying sizes
- Ordered Search: Search buckets from smallest to largest, dramatically reducing checks needed
- Hybrid Solver: Combines preprocessing (unit propagation, pure literal elimination) with RSAC
- Multiple Signature Types: Digital-root, Fibonacci, chaos map, cellular automata, fractal signatures
- Adaptive Method Selection: Automatically chooses best signature method for each problem type
- GPU Acceleration: Optional CUDA-based signature generation for massive problems
The repository includes comprehensive benchmarking suites:
- Basic benchmarks: Compare RSAC vs brute force on random 3-SAT
- Stress testing: Correctness, performance, and memory analysis
- SAT competition: Real-world instance compatibility
- Advanced variants: Multiple signature methods and optimizations
RSAC demonstrates practical improvements on:
- Random 3-SAT instances
- Structured satisfiable problems
- Phase transition instances
- Backdoor problems
- Graph coloring formulations
If you use RSAC in your research, please cite:
@article{betti2025rsac,
title={RSAC: Recursive Symbolic Attractor Computation for Exponential Search Space Reduction in Boolean Satisfiability},
author={Betti, Gregory},
journal={arXiv preprint arXiv:2025.XXXX},
year={2025}
}We welcome contributions! Please see our Contributing Guidelines for details.
- Fork the repository
- Create a feature branch (
git checkout -b feature/amazing-feature) - Commit your changes (
git commit -m 'Add amazing feature') - Push to the branch (
git push origin feature/amazing-feature) - Open a Pull Request
This project is licensed under the Apache License 2.0 - see the LICENSE file for details.
- The SAT solving community for foundational research
- Contributors to open-source SAT solvers and benchmarks
- The broader constraint satisfaction research community
Gregory Betti
Betti Labs
Email: gregory@betti-labs.com
GitHub: @Betti-Labs
⭐ Star this repository if RSAC helps your research!