MCP Solver

An MCP server for constraint solving (SAT, MaxSAT, SMT, CP, ASP). 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 (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.

Related MCP server: MCP Server Sample

Requirements

• Python 3.13

• 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:

git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
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.

How it works

The base mcp-solver package is a dependency-free solver helper library (mcp_solver.helpers.{pysat,maxsat,z3}; the CPMpy and Clingo 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.

Current status: in our runs with gpt-5.6-terra, all 26 test problems solve correctly. 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.