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](https://github.com/szeider/mcp-solver/tree/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.

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/](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==, 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 _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//

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

` 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"](https://doi.org/10.4230/LIPIcs.SAT.2025.30),

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.