Navokoj

A general-purpose engine for finding coherent structure inside astronomically large discrete spaces.

Actionable failures. Best-effort success. When perfect is impossible, we return the closest possible solution with precise diagnostics.

Start Solving Hugging Face

How It Works

Navokoj converts complex business planning into automated decisions.

Scheduling

Shift planning

→

Routing

Path optimization

→

Resources

Allocation

✓ High compliance with your business rules

Real Performance

Manual

Query

Navokoj

Compliance

Speed

Cost

✓ Automated decisions based on real data

✓ Faster planning cycles

API Integration

// Define your constraints

const result = await fetch('/v1/solve', {

constraints: "shifts ∧ skills",

optimize: "cost"

});

Typical response

< 2 seconds

Common Questions

📊

What industries?

Healthcare, logistics, manufacturing

🔌

Integration?

Simple REST API

⚡

How fast?

First call in < 5 mins

Learn More →

🔓

Open Source

github.com/sethuiyer/navokoj

The core Arithmetic Manifold framework — physics-inspired constraint solving in pure Python.

✓ Spectral operator mixing with prime weights
✓ Adiabatic cooling (exploration → exploitation)
✓ Native multi-valued logic (binary to k-ary)
✓ MAX-SAT optimization for overconstrained problems

Best for
Research, prototyping, learning the theory
Up to ~300 variables • 99%+ success rate

PRODUCTION

⚡

Commercial API

navokoj.shunyabar.foo

Production-grade engine with optimizations that push satisfaction to 100% whenever feasible.

✓ Grain boundary fixes for structured grids
✓ Arithmetic symmetry breaking at phase transitions
✓ GPU-accelerated for H100 / commodity hardware
✓ PSPACE-complete problems (QBF, Sokoban, Pebbling)

Production proven
92.57% on SAT 2024 Industrial Track (4,199 problems)
Up to 1M+ variables • 100% when satisfiable

What the production API has solved

3.2M clauses

R(6,6) N=35 Ramsey

2M clauses

K8s Placement

21/21 perfect

PSPACE problems

347ms median

vs 45s classical

129-SAT solved

8.6M variables

See It In Action

Videos & Demos

Watch the engine find coherent structure inside astronomically large discrete spaces in real-time.

Solving SAT with Quantum Vacuum Dynamics

Explore the innovative physics-inspired algorithms powering our engine.

The Solenoid and the Prime

Discover how numbers encode their own history through solenoidal dynamics and prime distribution.

Clause Density vs Performance

How solve time scales with problem complexity (clauses ÷ variables)

Source Data

Density	Median Time	Requests	Satisfaction
1-2 (sweet spot)	39ms	249	97.8%
2-3	189ms	259	99.8%
3-4	684ms	70	98.9%
4-5 (phase transition)	1.93s	107	98.2%
5-10	7.47s	59	99.7%
10-25 (Very Hard)	14.1s	31	95.4%
50+ (Monster)	16.2s	9	92.57%*

* Density 50+ includes 77,000-clause problems solved with 92.57% perfect solves. We convert number-theoretic phase transitions into computational leverage, solving SAT instances previously inaccessible to classical heuristics.

Real Performance. Real Results.

Verifiable witnesses for every claim. Production runs on H100 GPU ensembles.

100% SAT

⚡

129-SAT (Ultra-High-k)

Mean-field regime where CDCL search fails

Variables 200

Clauses 1,000,000

Satisfaction 100.0000%

Compute Time 9-10 min

Cost to compute $10.10

Per million clauses ~$0.01

100% SAT

🕸️

Ramsey R(5,5,5) N=52

3-edge-coloring with no monochromatic K₅

Variables 2.6M K₅ Cliques

Clauses 7.8M

Satisfaction 100.0000%

Compute Time 17 min

Cost to compute $17.10

Per million clauses ~$0.000002

✅ Proves R(5,5,5) > 52. Verifiable proof JSON provided.

92.15% SAT

📊

Random 3-SAT (1M Scale)

Critical density at α=4.26, industrial benchmark

Variables 1,000,000

Clauses 4.26M

Satisfaction 92.15%

Compute Time 171s

Cost to compute $3.35

Per million clauses ~$0.79

97.18% SAT

🏭

Supply Chain Optimization

Real-world logistics and inventory constraints

Variables 435,000

Clauses 1.3M

Satisfaction 97.18%

Compute Time 67.7s

Cost to compute $2.63

Per million clauses ~$2.02

99.93% SAT

📐

Ramsey R(3,3,3) N=20

Frustrated regime - 17 min

Variables 4,180 Clauses

Clauses 3 Violations

Satisfaction 99.93%

Compute Time 17 min

Cost to compute $16.89

Per million clauses -

α=4.26

📊

3-SAT Critical Density 45K

14 seconds, minimum charge

Variables 45,000

Clauses 191,700

Satisfaction 96.42%

Compute Time 14s

Cost to compute $1.50

Per million clauses -

Diagnostic Intelligence

DEFEKT: MRI for Constraints

Predict solvability before you solve. DEFEKT uses heuristic difficulty estimation to give you an MRI-style scan of your logical problem.

Cost Control

Avoid solver runs on likely unsatisfiable instances.

Constraint Debugging

Identify exactly why your problem is failing.

Smart Routing

Automatically select the right hardware and engine.

/v1/diagnose

Solvability Score 84%

Status Likely Solvable

Recommendation:

Use pro-deepthink on H100 GPU for optimal satisfaction.

Developer Experience

Integrate powerful constraint solving into your stack in minutes.

SAT Engine Endpoint

Submit raw CNF clauses, boolean expressions, or hybrid constraints. The engine automatically selects the best solver strategy (Nano, Mini, or Pro).

Method: POST
Endpoint: /v1/solve
Input: CNF, Boolean Logic, or Hybrid
Output: Assignment + Satisfaction Rate

Capabilities

Workforce Optimization: Shift planning, rostering
DevOps Logic: Dependency resolution, config validation
Resource Allocation: Load balancing, distribution

Use Case 1: Employee Scheduling (Python)

python

import requests

# 8 employees, 3 shifts, 7 days = 168 variables
payload = {
    "num_vars": 168,
    "clauses": [
        # Employee 1 must work at least one shift
        [1, 2, 3],
        # Cannot work morning AND afternoon (Mutually Exclusive)
        [-1, -2], [-2, -3], [-1, -3] 
        # ... more constraints
    ],
    "engine": "nano"
}

response = requests.post(
    "https://api.navokoj.shunyabar.foo/v1/solve",
    headers={"Authorization": "Bearer YOUR_KEY"}, 
    json=payload
)

Use Case 2: Microservices Orchestrator (cURL)

bash

"token function">curl "token operator">-X "token function">POST https://api.navokoj.shunyabar.foo/v1/solve \
  "token operator">-H "Authorization: Bearer YOUR_KEY" \
  "token operator">-d '{
  "expression": "
    ((gateway & (db_primary | db_replica)) -> services_ok)
    & ((auth ^ legacy) & (auth -> cache))
    & ((payment & fraud) <-> checkout)
    & ((orders | maint) & ~(orders & maint))",
  "solver": "pro"
}'

Use Case 3: Resource Allocation (JavaScript)

javascript

const response = await fetch('https://api.navokoj.shunyabar.foo/v1/solve', {
  method: 'POST',
  headers: {
    'Authorization': 'Bearer YOUR_KEY' 
  },
  body: JSON.stringify({
    expression: '(server_a | server_b) & (db_primary -> cache_warm)',
    solver: 'mini'
  })
});

const result = await response.json();
console.log(result.assignment); 
// {"server_a": 1, "db_primary": 1, "cache_warm": 1, ...}

Pay Per Solve. No Subscriptions.

Transparent pricing that scales with your needs. 50% India special applied automatically.

Standard Compute

For quick checks, validation, and small-scale problems.

$0.00

Free until June 2026, then $0.01 + $0.01/min (billed per-second, no rounding)

Hard cap: 5k variables, 35k clauses

Hard cap: 5k variables, 35k clauses
1k XOR vars, 500 nodes (Q-SAT)
Nano & Mini engines
Solvability Diagnostics & Diagnostics API
Concurrency: 2 requests (NP-complete solves)

Start Solving

L4 GPU

Production workloads. Faster convergence on complex problems.

$0.25

+ $0.10/min (billed per-second, no rounding)

Included limits (see table below)

Included: 100k variables, 300k clauses
10k XOR vars, 15k nodes (Q-SAT)
Pro engine (Chaotic Lotus Flow)
Industrial Scheduling (200 resources)
Concurrency: 3 requests (NP-complete solves)

Example: 10-minute solve $1.25

Start Solving

PRODUCTION

H100 GPU

Industrial-scale problems. Million-variable constraints.

$1.5

+ $1.00/min (billed per-second, no rounding)

Included limits (see table below)

Included: 1M variables, 8M clauses
100k XOR vars, 100k nodes (Q-SAT)
Ensemble engine (500 parallel jobs)
Global Scheduling (1,000+ resources)
Concurrency: 4 requests (NP-complete solves)

⚠️ Network Note: Sub-10s latency refers to H100 compute time. Large dataset transfer (>100MB) depends on your network.

Deploy H100

Service guarantees (alpha)

Status: Alpha. Self-serve tiers operate best-effort and may change limits, pricing, and behavior as reliability is hardened. No SLA is provided on self-serve tiers yet.

Enterprise SLA + support is on the roadmap. If you need contractual uptime, dedicated capacity, longer runtimes, or spend caps, contact rxgtoing@gmail.com.

Billing: runtime is billed per-second (fractional). No rounding. If a solve hits the timeout, we still return the best partial result found so far.

30-Minute Timeout Guarantee

To ensure fair bandwidth usage, all solves have a hard timeout of 30 minutes. However, we always return the best partial result found so far, never an empty error. (Note: Our average solve time is milliseconds. 30 minutes is a p99 extreme edge case.)

Need longer runtimes? For dedicated 3-5 hour runs, contact rxgtoing@gmail.com.
Enterprise Pricing: $100 base + $10/hour.

Full Hardware specifications & API Limits

Constraint Metric	Standard (CPU)	L4 GPU	H100 GPU
Included Boolean variables	5,000	100,000	1,000,000
Included Boolean clauses	35,000	300,000	8,000,000
Included XOR-SAT variables	1,000	10,000	100,000
Included XOR constraints	500	5,000	50,000
Included Q-SAT nodes	500	15,000	100,000
Included states per node	5	20	50
Included scheduling resources	20	200	1,000
Hourly Request Limit	100	500	Unlimited*
Concurrent Jobs	2	3	4

Search space at included limits

Model	Standard (CPU)	L4 GPU	H100 GPU
Boolean SAT	2⁵⁰⁰⁰ ≈ 10¹⁵⁰⁵	2¹⁰⁰⁰⁰⁰ ≈ 10³⁰¹⁰³	2^1000000 ≈ 10³⁰¹⁰³⁰
XOR-SAT	2¹⁰⁰⁰ ≈ 10³⁰¹	2¹⁰⁰⁰⁰ ≈ 10³⁰¹⁰	2¹⁰⁰⁰⁰⁰ ≈ 10³⁰¹⁰³
Q-SAT (k-ary)	5⁵⁰⁰ ≈ 10³⁵⁰	20¹⁵⁰⁰⁰ ≈ 10¹⁹⁵¹⁵	50¹⁰⁰⁰⁰⁰ ≈ 10¹⁶⁹⁸⁹⁷

These numbers illustrate the size of the full assignment space at the included variable limits. Real difficulty depends on structure, not just size.

CPU limits are hard caps. L4/H100 are included limits. Concurrency is intentionally low (2–4) because these are NP-complete solves. * H100 hourly limits are subject to inventory availability and account standing.

Frequently Asked Questions

Common questions about Navokoj and constraint solving.

Engine Benchmarks

Detailed performance metrics across 4,199 industrial SAT instances.

Engine	Satisfaction Rate	Speed	Quality	Use Case
PRO	92.57%	7.90/sec	99.92%	Mission-critical verification
MINI	31.37%	10.64/sec	99.55%	Balanced optimization
NANO	3.24%	Ultra-fast	96.41%	Real-time feedback

Navokoj

How It Works

Real Performance

API Integration

Common Questions

Open Source Core + Production API

Open Source

Commercial API

Videos & Demos

Solving SAT with Quantum Vacuum Dynamics

The Solenoid and the Prime

Clause Density vs Performance

Source Data

Real Performance. Real Results.

129-SAT (Ultra-High-k)

Ramsey R(5,5,5) N=52

Random 3-SAT (1M Scale)

Supply Chain Optimization

Ramsey R(3,3,3) N=20

3-SAT Critical Density 45K

DEFEKT: MRI for Constraints

Developer Experience

SAT Engine Endpoint

Capabilities

Pay Per Solve. No Subscriptions.

Standard Compute

L4 GPU

H100 GPU

Service guarantees (alpha)

30-Minute Timeout Guarantee

Full Hardware specifications & API Limits

Search space at included limits

Frequently Asked Questions

Engine Benchmarks