Deep-Tech Research Lab
Unapologetically ambitious, practically useful, Foundational Deep-Tech research lab from
India.
Computation is physics, and constraint solving is thermodynamic equilibration. ShunyaBar Labs develops
constraint solvers that treat Boolean satisfiability and combinatorial optimization as continuous physical
systems rather than discrete search problems.
Visit shunyabar.foo
|
Labs documentation
Behavioral Quotients — the unifying paper
Behavioral Quotients as a Design Principle for Computation: Geometry, Compression, and Commitment — a common lens and design criterion for state reduction, stated against prior art (Myhill–Nerode, causal-state minimality, exact state aggregation, final-coalgebra universal property). The solver line is a reference implementation whose correctness results are externally verified, and every cross-regime bridge is marked as a consequence, an analogy, or a conjecture.
Read the paper
|
PDF
STOP Operators — resolution at finite scale
STOP Operators as Resolution Flows on Infinite Computational Paths. An infinite path is observed at finite resolution rather than evaluated only at its limit. Geometric stopping reproduces Abel summability — the Abel parameter is the observer's survival probability — and the finite part of a polynomial divergent path splits into a spectral term plus an observer correction: FP = ζ(−m) + 1/(m+1). Offered as a research program, not a classification: the core results are standard-analysis consequences, and the open problem is which arithmetic structures survive all fair observers.
Read the manuscript
Three papers, one principle
These share a single design principle — distinguish what matters from what does not, at a chosen resolution — and a single evidence standard: every claim carries its tier, and each tier states what it does not license. They are not a unified theory.
- The quotient — minimal state as histories modulo future indistinguishability. Design principle + partial theorems; the transfer theorem is open.
- The completion — the space of those quotients, when the continuation set is infinite, is simultaneously a metric completion, an inverse limit, and a hyperbolic boundary. Construction + completion theorem; much of the surrounding machinery is standard and the paper says so.
- The observer — a path at finite resolution is a survival-weighted observable whose regularized value splits into spectral residue plus observer correction. Research program; the core results are standard-analysis consequences, and observer invariance is undefined as yet for arithmetic paths.
Quotient, completion and expectation are three different operations on related objects — not one operation at three scales.
Evidence & verification
Correctness claims ship with the material to check them: hashed instances, per-solve artifacts, and verifiers kept separate from the solver.
- Evidence pack — 9.4 GB / 8,737 files:
MANIFEST.sha256, 557 MB of CNF instances, per-engine result JSONs, GPU campaign results, instance generators, and two audit reports.
huggingface.co/buckets/sethuiyer/shunyabar-evidence-v1
- Independent verifiers — clause-level assignment checkers plus a reproducibility harness, run against the original instance rather than the solver's own counter.
- Worked example — hospital rostering: 39,842 / 39,842 clauses satisfied, all five domain checks pass (exact cover, at most one shift per nurse per day, max consecutive working days, incompatible pairs, senior night coverage), instance SHA-256 recorded. The nurse-rostering run reports 0 hard violations and 31 soft violations rather than claiming perfection.
Baseline comparison — including where we lose
Head-to-head against Kissat 4.0.4, Open-WBO 2.1, HiGHS, UWrMaxSat 2.0.6 (CaDiCaL-based), Aperture (MSE 2026 weighted-anytime champion) and EvalMaxSAT — every returned witness re-verified clause-by-clause. The result is per-family, not a blanket win:
- Structured / planted SAT → we lose. Kissat is 5–200× faster.
- Random 3-SAT at the phase transition → faster time-to-model (100–1000× when it solves), but incomplete (12/14 vs 14/14) and worse under PAR-2.
- Weighted MaxSAT → lower verified cost on the tested families, ~1000× faster; the margin against a current solver is 9–104%, not orders of magnitude.
- Placement family → we plateau at 2.6× the verified optimum (351 vs 137) and hit a repair fixed point rather than continuing to improve.
The claim that survives is narrow: a budget-bounded, hard-constraint-preserving, monotone-improving, independently verifiable incumbent — not optimality, and not a proven general speedup. MaxHS remains an open baseline (CPLEX-gated).
NitroSAT
Physics-informed MaxSAT approximator with tri-state outputs that distinguish proven,
disproven and unknown rather than forcing a binary claim. Streams tens of millions of clauses with bounded
memory. Open source (C99, Apache 2.0), with the full evidence pack linked above.
SAT Solver
Prime Weights
C + LuaJIT
View NitroSAT
BAHA
An optimizer that detects thermodynamic phase transitions. When algorithms freeze,
BAHA computes the exact escape path using Lambert-W branch enumeration. Deterministic basin-hopping replaces
random restarts.
Optimization
Thermodynamics
C++
View BAHA
View Casimir SAT Solver
Multiplicative PINNs
Constraint learning without gradient conflict. Euler product gates align physics and
data losses. Solves the gradient pathology problem, dropping conflicts from 45% to just 2%.
Physics-Informed NNs
CFD
Python
View Multiplicative PINNs
Navokoj API
Enterprise constraint intelligence platform. GPU-accelerated API with six engines
(Nano, Mini, Pro, Hybrid, Q-State, Zeta). Includes DEFEKT diagnostics for pre-solve analysis and solvability
prediction.
Enterprise
GPU-accelerated
API
View Navokoj
FUTCache
A bounded-memory sufficient-state representation of explored geometry. Approximate metric quotienting collapses near-duplicate states into representatives, so a search frontier can be cached instead of re-derived.
Metric Quotienting
C
Trace Validation
View FUTCache
FactorAgent
Invariant-preserving agent harnesses. OTP supervision, arithmetic security lattices, and lawful composition — tool calls are denied by default and authority is evaluated per action, with an append-only audit log.
Agent Runtime
Elixir/OTP
Authorization
View FactorAgent
Novelty Geometry
The Geometry of Endless Discovery — resolution-depth ordered-discovery completion. Main result: metric completion of ordered novelty = inverse-limit completion = hyperbolic boundary. Minimal online novelty memory is a Myhill–Nerode future-equivalence quotient.
Topology
Ultrametric
Zenodo DOI
View Novelty Geometry
