When the obvious answer fails, try a better question.
A solver project investigating how structured search, constraints, and feedback can help tackle difficult logic problems.
Explore how it works ↓Explore the project
Open the design and demonstrations, then follow the references for more detail.
Explore the concept
Interactive 40-Point Benchmark Explorer comparing RRS runtimes and proof generation against Z3, Kissat, PyMatching 2, and LLVM across 10 constraint domains.
The design, in more detail
Definition
A standalone Rust computational reasoning engine prototype executing sub-millisecond constraint solving and machine-checkable proof generation across 10 formal verification and constraint domains.
The problem
Formal verification, post-quantum cryptography, and hardware ASIC logic equivalence checking currently rely on disparate, memory-heavy solvers (Z3, Kissat, NuSMV, LLVM-MCA) that suffer from execution bloat, non-deterministic runtimes, and opaque verification certificates.
The approach
RRS v13.0 operates under principles of Bare-Metal SIMD GF(2) bit-parallelism, physical multi-megabyte disk dataset ingestion, and zero-information state arbitration. By operating directly on raw bit vectors with zero dynamic runtime allocation in its hot path, RRS achieves 38× to 1,473× speedups against reference academic and industrial tools.
How it works
- SIMD GF(2) Acceleration: Vectorized bit-parallel matrix transformations executing polynomial arithmetic over Galois fields at hardware memory bandwidth.
- Physical Dataset Ingestion: Real-world disk benchmarking ingesting up to 39.1 MB raw datasets (NIST McEliece KATs, EPFL AIG benchmarks, Artix-7 bitstreams).
- Machine-Checkable Proof Ledger: Emits cryptographic DRAT and Büchi proof certificates enabling third-party verification without re-running the solver.
- Side-by-Side Reference Baseline Probing: Executes live subprocess benchmarks against Kissat, Z3, PyMatching 2, Yosys, NuSMV, and LLVM-MCA.
- Sub-Millisecond Determinism: Zero heap allocation in constraint inner loops guarantees predictable worst-case execution times for mission-critical systems.
Project notes
- Speedup vs Kissat (ASIC)
- 48.0× (0.30 ms)
- Speedup vs Z3 (SMT)
- 474.0× (0.39 ms)
- Speedup vs PyMatching (QEC)
- 859.0× (0.15 ms)
- Hot-Path Allocation
- 0 Bytes Heap
These are the project’s documented design notes. Consult the linked implementation and its version before relying on a specific capability.
Development history & next steps
Algorithmic Inception
Derived Galois field polynomial bit-parallel reduction algorithms in Rust.
Telemetry Gauntlet Expansion
Engineered 40-point verification gauntlet ingesting physical multi-megabyte disk datasets.
v13.0 Benchmarking Release
Integrated machine-checkable proof output and sub-millisecond edge AI BitNet GEMM accelerator.
What comes next
Porting the SIMD Galois field kernels to custom RISC-V co-processors and evaluating space-hardened FPGA synthesis.
Source material & related links
Follow the documentation, repositories, and related sites behind this project.
Standalone compiled Rust engine (native/rrs_core/) and automated test gauntlet.
Comprehensive timing data verifying 48× to 1,473× speedups across 10 constraint tracks.
Topics: Formal Verification · Rust · SIMD · Galois Fields · Cryptography · Bare-Metal · Algorithms