SAT Solving

Classic Boolean satisfiability: hand in a DIMACS CNF file and get a sat / unsat verdict. Same billing, polling, and MCP access as the rest of the platform. For richer logic with models, use the SMT endpoint.

Quickstart

Submit a DIMACS CNF problem:

curl -X POST https://api.mcpte.ch/v1/sat \
  -H 'Content-Type: application/json' \
  -d '{"problem":"p cnf 3 2\n1 0\n-2 3 0\n","format":"dimacs"}'

Returns a job id:

{ "job_id": "0191cc2e-...+", "status": "queued" }

Poll for the result:

curl https://api.mcpte.ch/v1/jobs/{job_id}

{ "status": "completed", "result": { "sat": true } }

Endpoints

Results

Results return "sat": true or "sat": false. If the solver cannot decide, "sat": null with an error message — that is not the same as unsat.

For assignment models and unsat cores, use the SMT endpoint with (get-model) or a requested core.

Authentication

MCP

A native Model Context Protocol server is available at https://api.mcpte.ch/v1/mcp using the Streamable HTTP transport. Use it from Claude Desktop, Cursor, and other MCP clients — it handles JSON parsing and result polling for you, and this endpoint is available as a tool.