mcp-solver

An MCP server for constraint solving (SAT, MaxSAT, SMT, CP, ASP, DP). It turns the connected LLM host into a solver-writing agent: the host gets a Python kernel preloaded with a real solver library, modeling instructions for the chosen backend, and a submission gate. The host encodes the problem, runs and verifies it against the real solver, and submits the final program — the outcome is the solution plus the verified solver program that produced it.

Version 4 is a complete re-architecture. Both the MCP interface and the solving engine changed; the design from the SAT 2025 paper (v3) lives on unchanged on the v3 branch. See From v3 to v4 below.

mcp-solver-serve runs over stdio and works with any MCP host: Claude Desktop, Claude Code, Cursor, or your own client. The host LLM does the solving itself — the server is a solver toolkit; it runs no LLM and needs no API key:

• select_backend(solver) sets up a persistent IPython kernel with the backend's solver library and helper functions, and returns the modeling instructions for that backend. Calling it again recycles the kernel for the next problem.
• Kernel tools (python_exec, python_reset, python_status, python_interrupt) let the host write, run, and verify a real solver program; bare python_exec calls are routed to the solving kernel automatically.
• submit_code(code) is the finish line: the final self-contained program is syntax-checked and, on success, stored and linked back as an MCP resource (mcp-solver://submissions/{id}), with the verdict as structured content.
• Resources: mcp-solver://guide (backend selection and workflow) and mcp-solver://template/{solver} (the full modeling instructions, browsable without selecting).
• Statistics (optional): set MCP_SOLVER_STATS=/path/to/stats.jsonl in the server's env to log one JSON line per solving episode — tool-call counts, execution failures, submissions, wall time. Host tokens are invisible to the server by protocol design; tool usage is the comparable metric across hosts. (submit_code results also carry a compact stats snapshot as structured content; the CLI path reports tokens and actual OpenRouter cost via --stats-json.)

Claude Desktop configuration (once the PyPI name transfer completes — see Installation):

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uvx",
      "args": ["--from", "mcp-solver[agent]", "mcp-solver-serve"]
    }
  }
}

From a checkout (the working setup today, and the development path always):

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uv",
      "args": ["run", "--project", "/path/to/mcp-solver", "mcp-solver-serve"]
    }
  }
}

The server needs no API key — the model doing the solving belongs to the host. An OpenRouter key is required only for the command-line path below, which brings its own agent.