Both Hemispheres
Paid APIs and research tooling
Both Hemispheres offers two sellable services on the same account balance: a scalable SAT solving workflow for DIMACS CNF files and an OpenAI-compatible LLM API running on owned GPUs.
Logic
Upload DIMACS CNF files up to 100 MB, run them in a single solver thread for up to one hour, and pay only if a SAT assignment is found and you want to view or download it. SAT assignment pricing is $10 per 10 million variables.
Open SAT serviceLanguage
Use the current OpenAI-compatible LLM endpoint with prepaid credits, model catalog visibility, and a browser-based chat playground.
Open LLM serviceProof
Enter assumptions and a goal in free text, let the hosted LLM translate them to SMT-LIB, solve them with Bitwuzla on the worker, and read back a school-book style proof.
Open theorem demoAccount
No stored session yet.
Use the same prepaid balance for SAT unlocks and LLM API usage.
Create or import an API key to load the customer account.
No capacity requests yet.
No capacity request submitted yet.
Service 1
Upload a DIMACS CNF file, run it with a one-hour limit on a single solver thread, and pay only when a SAT solution exists and you want the variable assignment. SAT assignment pricing is $10 per 10 million variables.
No SAT job selected.
Service 2
Use the existing OpenAI-compatible chat API with prepaid credits on the same account.
No completion yet.
Service 3
Describe assumptions and a goal in free text. The system uses the hosted LLM to draft SMT-LIB, runs Bitwuzla with CryptoMiniSat on the worker, and renders the resulting proof as readable markdown.
No theorem proof yet.
No theorem run yet.
Infrastructure