szeider/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.
The MCP server
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, from a checkout (the working setup today, and
the development path always; see Installation):
Once the PyPI name transfer completes, no checkout will be needed. Until then
this configuration fetches an unrelated stale v2.0.0 upload, so do not use it
yet:
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.
Requirements
- Python 3.13 or 3.14 (not yet 3.15: the solver kernels run on the server's
Python version, and ortools and python-sat publish no 3.15 wheels yet)
- uv (a hard runtime requirement: solver
libraries are supplied at solve time via uv run --with)
- An OpenRouter API key — for the CLI and benchmark
harness only; the MCP server itself runs without one
Installation
> **v4 is not yet installable from PyPI.** The PyPI name mcp-solver is
> held by a third-party upload of stale v2.0.0 code, and PyPI blocks
> confusably similar names; a PEP 541
> name-transfer request is pending. Until it resolves, install from a
> checkout:
See INSTALL.md for details and troubleshooting.
Command-line use
The mcp-solver CLI runs the same solving pipeline without an MCP host,
which is handy for scripts and benchmarks:
The solution JSON goes to stdout; the submitted solver program (e.g.
n_queens_code.py) and a complete run log (run_*.json) land in the working
directory.
| Option | Description |
| ---------------- | ------------------------------------------------------ |
| --problem FILE | Read the task from a markdown file instead of text |