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
v3branch. 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; barepython_execcalls 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) andmcp-solver://template/{solver}(the full modeling instructions, browsable without selecting). - Statistics (optional): set
MCP_SOLVER_STATS=/path/to/stats.jsonlin the server'senvto 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_coderesults 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):
{
"mcpServers": {
"mcp-solver": {
"command": "uv",
"args": ["run", "--project", "/path/to/mcp-solver", "--extra", "agent", "mcp-solver-serve"]
}
}
}
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:
{
"mcpServers": {
"mcp-solver": {
"command": "uvx",
"args": ["--python", "3.14", "--from", "mcp-solver[agent]", "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.
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-solveris 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:
git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv # Python 3.13 or 3.14, per pyproject.toml
uv pip install -e ".[agent]"
# OpenRouter key — only needed for the CLI path, not the MCP server:
mkdir -p ~/.config/coder
echo 'OPENROUTER_API_KEY="sk-or-v1-..."' > ~/.config/coder/.env
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:
mcp-solver pysat "Place 8 non-attacking queens on an 8x8 board and give one solution."
mcp-solver pysat --problem tests/problems/pysat/n_queens.md
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.
From an editable clone, the CLI runs in dev mode: helpers and templates come from the source checkout (auto-detected), with one provenance line on stderr.
mcp-minion
The CLI runs mcp-minion underneath: a minimal ReAct agent over MCP,
developed in this repo as the workspace package minion/. It is
a lightweight, batchable substitute for a full MCP host such as Claude
Desktop — point its standalone CLI at mcp-solver-serve (or any MCP server)
to script what a chat host would do interactively (see
minion/README.md). The default agent model is
gpt56terra, the bundled alias for OpenRouter's openai/gpt-5.6-terra.
Backends
Each backend is selected as the first CLI argument (or via the
select_backend tool). The right solver library is injected into the
solve-time kernel automatically.
MiniZinc mode from v3 is retired; constraint programming is now covered by
CPMpy. The didp backend is based on domain-independent dynamic programming
(Kuroiwa & Beck; solved with
didppy's anytime beam search): problems are
modeled as state transition systems, a natural fit for routing, sequencing,
scheduling, and packing.
How it works
The base mcp-solver package is a dependency-free solver helper library
(mcp_solver.helpers.{pysat,maxsat,z3}; the CPMpy, Clingo, and DIDP
backends need no helper module). It is never pip-installed into your
environment; instead it is injected into each solve-time kernel via
uv run --with mcp-solver==<version>, alongside the backend's solver library.
This keeps the host environment clean and each solve reproducible.
Each backend ships a project template: a markdown prompt (package data)
with the encoding conventions, output format, and helper API for that
solver. The template goes to whoever solves: an MCP host receives it from
select_backend; the CLI hands it to its mcp-minion agent as the system
prompt. Either way, the solving LLM drives the write → execute → verify
loop in a persistent IPython kernel — the ipython_mcp server from
agentic-python-coder —
and must end the solve by calling submit_code with the final
self-contained program (syntax-checked server-side, never written to disk
by the kernel). On the MCP path the accepted submission is linked back to
the host as a resource; on the CLI path the client extracts the last
successful submission, writes it to <basename>_code.py, and re-executes
it in a fresh uv kernel to produce the answer.
Benchmark harness
mcp-solver-bench runs the bundled test problems in tests/problems/<solver>/
end-to-end and validates each result against a per-problem
*_ground_truth.py validator (which reads the solution JSON on stdin and
returns {"valid": ..., "message": ...}).
# Benchmark every backend
mcp-solver-bench
# Specific backends, several runs each, in parallel
mcp-solver-bench pysat z3 --runs 3 --jobs 4
Each run is bounded by --step-limit (default: 30 agent steps), and results
are appended to results.jsonl in the output directory.
The same problems are also runnable as pytest end-to-end tests
(uv run pytest minion/e2e_tests -k didp), and mcp-solver-runfolder <solver> <problem> <dir> materializes a standalone mcp-minion run folder
for any of them.
Current status: in our runs with gpt-5.6-terra, all 30 bundled test
problems solve correctly, including the four didp problems (TSPTW,
knapsack, weighted tardiness, talent scheduling), each solved to proven
optimality in every run. The MCP server path is validated with Claude Opus
as host: 229/229 instances across
CP-Bench (101) and
ASP-Bench (128) solve correctly
under strict semantic validation, as do the bundled SAT, MaxSAT, and SMT
problems.
From v3 to v4: a new architecture
The SAT 2025 paper, "Bridging Language Models and Symbolic Solvers via the
Model Context Protocol",
documents v3: an MCP server exposing model-editing tools (add_item,
replace_item, solve_model, …) through which a chat LLM builds up a solver
model item by item, with solving happening inside the server.
v4 follows the IPython-kernel approach laid out in the CP-Agent (LLM4Code 2026) and ASP-Bench (NSE '26) papers: instead of a host LLM editing a model through protocol tools, a dedicated coding agent works in a persistent IPython kernel, where it iteratively writes an actual Python solver program, executes it against the real solver, verifies the result independently, and only then submits the program as the answer.
Citations
- Stefan Szeider, "Bridging Language Models and Symbolic Solvers via the Model Context Protocol", SAT 2025. Documents the v3 architecture (v3 branch). DOI 10.4230/LIPIcs.SAT.2025.30
- Stefan Szeider, "CP-Agent: Agentic Constraint Programming", in Proceedings of the 3rd International Workshop on Large Language Models For Code (LLM4Code 2026), pages 6–13, ACM, 2026. The IPython-kernel approach behind v4. DOI 10.1145/3786181.3788711
- Stefan Szeider, "ASP-Bench: From Natural Language to Logic Programs", in Proceedings of the 2026 IEEE/ACM 2nd International Workshop on Neuro-Symbolic Software Engineering (NSE '26), pages 1–8, ACM, 2026. The verification-gated benchmark methodology used by v4's test problems. DOI 10.1145/3786168.3788402
License
MIT; see LICENSE.
