Integrate AI with Constraint Solvers

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 (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/. 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