Pricing

Clear public pricing for reasoning workloads

Both Hemispheres uses a simple prepaid-credit model. The current public offer focuses on SAT solving and an OpenAI-compatible LLM API, with a theorem lane priced as a lightweight preview tier rather than a full enterprise proving product.

Public Offer

Current product pricing

Scalable SAT Solver

Upload up to `100 MB`, run a one-hour single-thread job, and pay only when a satisfying assignment exists and you want to unlock it.

`SATISFIABLE`: `$10` per `10,000,000` distinct clause variables to unlock the assignment
`UNSATISFIABLE`: visible for free
`UNKNOWN`: visible for free

LLM API

OpenAI-compatible prepaid inference and async batch jobs on the public Llama offer.

Prompt tokens: `$0.50 / 1M`
Completion tokens: `$0.50 / 1M`
Async chat and embeddings batches use the same underlying model pricing
Shared prepaid balance with the SAT service

Theorem Proving Harness

The theorem harness is a preview-priced reasoning surface for solver-backed proof workflows.

First `20` solver-backed runs per customer per month included
Then `$0.05` per additional solver-backed theorem run
Underlying theorem-harness LLM token usage is still billed on the normal LLM lane
Unsupported theorem translations do not consume the theorem run quota

Reserved capacity / dedicated deployments

Monthly quote-based offers are now available for buyers who need predictable capacity, private lanes, or a dedicated deployment. Submit the request from the authenticated account area and it will be reviewed manually. Accepted deals can also be routed through a dedicated upstream lane when the workload needs stronger isolation.

Quote-based monthly pricing
Reserved-capacity and dedicated-deployment request flow is live
Accepted deals can now be provisioned as private model aliases on the standard API surface
Included monthly token budgets can now be enforced with either metered overage or hard blocking
Dedicated-upstream routing is now available in first iteration for accepted private aliases

Notes

What buyers should know

Pricing is designed for low-friction evaluation first, with quote-based recurring offers available through the account request workflow.
The same balance can be used across the public SAT and LLM services.
SAT unlock pricing scales linearly with the number of distinct absolute variable IDs actually used in clauses, not just the `p cnf` header.
If you need a custom benchmark, reserved lane, or dedicated deployment, submit a capacity request from the account area or contact support.
If a billing issue appears, contact support and the issue can be reviewed manually.

Next Step

Start with trial credits and test one real workload

The fastest way to evaluate the price-to-value ratio is still a live run on your own CNF instance or your own prompt flow.

Start with trial credits See benchmarks