MCP Solver

MCP Solver

用于约束求解（SAT、MaxSAT、SMT、CP、ASP、DP）的 MCP 服务。它会将连接的 LLM 宿主转变为编写求解器的 Agent：宿主会获得一个预加载了真实求解器库的 Python 内核、所选后端的建模说明以及提交关卡。宿主对问题进行编码，使用真实求解器运行并验证，然后提交最终程序——最终结果是解，以及生成该解且经过验证的求解器程序。

版本 4 是一次完整的重新架构。 MCP 接口和求解引擎都已更改；SAT 2025 论文（v3）中的设计仍原样保留在 v3 分支中。 请参阅下文的 从 v3 到 v4。

MCP 服务

mcp-solver-serve 通过 stdio 运行，适用于任何 MCP 宿主：Claude Desktop、Claude Code、Cursor 或你自己的客户端。宿主 LLM 自行完成求解——服务是一个求解器工具包；它不运行 LLM，也不需要 API 密钥：

• select_backend(solver) 会设置一个持久的 IPython 内核，其中包含后端的求解器库和辅助函数，并返回该后端的建模说明。再次调用时，会重置内核以处理下一个问题。
• 内核工具（python_exec、python_reset、python_status、 python_interrupt）允许宿主编写、运行并验证真实的求解器程序；单独调用 python_exec 时，会自动路由到求解内核。
• submit_code(code) 是最后一步：最终的独立程序会经过语法检查，检查通过后将被存储，并作为 MCP 资源链接回来（mcp-solver://submissions/{id}），同时返回结构化内容中的判定结果。
• 资源： mcp-solver://guide（后端选择和工作流）以及 mcp-solver://template/{solver}（完整的建模说明，无需选择后端即可浏览）。
• 统计信息（可选）：在服务的 env 中设置 MCP_SOLVER_STATS=/path/to/stats.jsonl，即可为每个求解过程记录一行 JSON——工具调用次数、执行失败、提交次数、耗时。根据协议设计，宿主的令牌对服务不可见；工具使用情况是不同宿主之间可比较的指标。（submit_code 的结果也会在结构化内容中附带精简的统计快照；CLI 路径通过 --stats-json 报告令牌数和实际的 OpenRouter 费用。）

通过代码库检出配置 Claude Desktop（这是目前可用的设置方式，也是始终适用的开发方式；参见安装）：

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uv",
      "args": ["run", "--project", "/path/to/mcp-solver", "--extra", "agent", "mcp-solver-serve"]
    }
  }
}

PyPI 名称转让完成后，就无需检出代码库了。在此之前，此配置会获取一个无关的过时 v2.0.0 上传包，因此暂时不要使用：

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uvx",
      "args": ["--python", "3.14", "--from", "mcp-solver[agent]", "mcp-solver-serve"]
    }
  }
}

服务不需要 API 密钥——执行求解的模型属于宿主。只有下文的命令行用法需要 OpenRouter 密钥，因为该路径自带 Agent。

要求

• Python 3.13 或 3.14（暂不支持 3.15：求解器内核在服务端的 Python 版本上运行，而 ortools 和 python-sat 尚未发布 3.15 轮子包）
• uv（运行时硬性要求：通过 uv run --with 在求解时提供求解器库）
• OpenRouter API 密钥——仅用于 CLI 和基准测试工具；MCP 服务本身不需要密钥即可运行

安装

v4 尚不能从 PyPI 安装。 PyPI 名称 mcp-solver 被第三方上传的过时 v2.0.0 代码占用，且 PyPI 会阻止容易混淆的相似名称；目前正在等待 PEP 541 名称转让申请获批。在此之前，请从代码库检出安装：

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

详情和故障排除请参阅 INSTALL.md。

命令行用法

mcp-solver CLI 可在没有 MCP 主机的情况下运行相同的求解流程， 适用于脚本和基准测试：

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

求解结果 JSON 会输出到 stdout；提交的求解器程序（例如 n_queens_code.py）和完整的运行日志（run_*.json）会保存到工作目录中。

选项	说明
--problem FILE	从 markdown 文件读取任务，而不是从文本读取
--model NAME	Agent 模型：可使用 gpt56terra 这样的别名，或完整的 OpenRouter ID（默认值：gpt56terra）
--workdir DIR	运行的工作目录（默认值：当前目录）
--step-limit N	停止前允许的最大 Agent 步数（默认值：30）
-q, --quiet	不显示每步的进度输出
--dev [PATH]	开发模式：从本地检出版本获取辅助程序和模板（单独使用 --dev 时自动检测；在检出版本内会自动启用；也可通过 MCP_SOLVER_DEV 启用）
--no-dev	禁用开发模式；使用已发布的辅助程序（固定为 PyPI 版本）
--stats-json FILE	将运行统计信息以 JSON 格式写入 FILE

从可编辑克隆版本运行时，CLI 会处于开发模式：辅助程序和模板来自源代码检出版本（自动检测），并会在 stderr 输出一行来源信息。

mcp-minion

CLI 在底层运行 mcp-minion：一个精简的 MCP ReAct Agent，作为工作区软件包 minion/ 在此仓库中开发。它是完整 MCP 主机（例如 Claude Desktop）的轻量级、可批处理替代方案——将其独立 CLI 指向 mcp-solver-serve（或任何 MCP 服务），即可通过脚本实现聊天主机的交互操作（参见 minion/README.md）。默认 Agent 模型为 gpt56terra，这是 OpenRouter 的 openai/gpt-5.6-terra 的内置别名。

后端

每个后端都通过 CLI 的第一个参数（或 select_backend 工具）选择。相应的求解器库会自动注入求解时内核。

后端	领域	求解器库
pysat	布尔可满足性（SAT）	python-sat
maxsat	加权优化	python-sat (RC2)
z3	SMT 求解 / 验证	z3-solver
cpmpy	约束规划（CP）	cpmpy
clingo	答案集编程（ASP）	clingo
didp	动态规划（DIDP）	didppy

v3 起的 MiniZinc 模式已弃用；约束规划现在由 CPMpy 支持。didp 后端基于领域无关动态规划 （Kuroiwa & Beck；使用 didppy 的 anytime beam search 求解）：问题被建模为状态转换系统，非常适合路径规划、排序、调度和装箱问题。

工作原理

基础 mcp-solver 包是一个无依赖的 求解器辅助库 （mcp_solver.helpers.{pysat,maxsat,z3}；CPMpy、Clingo 和 DIDP 后端不需要辅助模块）。它不会通过 pip 安装到你的 环境中；而是在每次求解时，通过 uv run --with mcp-solver==<version> 注入到内核中， 并同时注入后端的求解器库。 这样可以保持宿主环境干净，并确保每次求解都可复现。

每个后端都附带一个 项目模板：一份 Markdown 提示词（包数据）， 其中包含该求解器的编码约定、输出格式和辅助 API。模板会提供给求解者：MCP 宿主通过 select_backend 获取模板；CLI 则将其作为系统 提示词交给 mcp-minion Agent。无论哪种方式，负责求解的 LLM 都会在持久化的 IPython 内核中驱动 编写 → 执行 → 验证循环——该内核由 agentic-python-coder 中的 ipython_mcp 服务提供——并且必须在求解结束时调用 submit_code，提交最终的 自包含程序（由服务端进行语法检查，内核绝不会将其写入磁盘）。在 MCP 路径中，已接受的提交会作为资源关联回宿主；在 CLI 路径中，客户端会提取最后一次成功提交，将其写入 <basename>_code.py，并在全新的 uv 内核中重新执行，以生成答案。

基准测试工具

mcp-solver-bench 会端到端运行打包的测试问题（位于 tests/problems/<solver>/），并使用每个问题对应的 *_ground_truth.py 验证器验证结果（该验证器从标准输入读取解的 JSON，并 返回 {"valid": ..., "message": ...}）。

# Benchmark every backend
mcp-solver-bench

# Specific backends, several runs each, in parallel
mcp-solver-bench pysat z3 --runs 3 --jobs 4

每次运行都受 --step-limit 限制（默认：30 个 Agent 步骤），结果 会追加到输出目录中的 results.jsonl。

同一批问题也可以作为 pytest 端到端测试运行 （uv run pytest minion/e2e_tests -k didp），而 mcp-solver-runfolder <solver> <problem> <dir> 会为其中任意问题生成独立的 mcp-minion 运行文件夹。

当前状态：在我们使用 gpt-5.6-terra 的测试中，全部 30 个打包测试 问题均能正确求解，其中包括四个 didp 问题（TSPTW、 knapsack、weighted tardiness、talent scheduling）；每次运行都能求得经证明的最优解。MCP 服务路径已使用 Claude Opus 作为宿主进行验证：在 CP-Bench（101 个）和 ASP-Bench（128 个）中，共 229/229 个实例均通过严格的语义验证并正确求解；打包的 SAT、MaxSAT 和 SMT 问题也同样如此。

从 v3 到 v4：全新架构

SAT 2025 论文《通过模型上下文协议连接语言模型与符号求解器》介绍了 v3：一个 MCP 服务，通过模型编辑工具（add_item、replace_item、solve_model 等）供聊天大模型调用，由其逐项构建求解器模型，并在服务内部进行求解。

v4 采用了 CP-Agent（LLM4Code 2026）和 ASP-Bench（NSE '26）论文提出的 IPython 内核方案：专用编码 Agent 不再通过协议工具编辑模型，而是在持久化的 IPython 内核中工作，迭代编写实际的 Python 求解器程序，针对真实求解器执行程序，独立验证结果，最后才将程序作为答案提交。

	v3（SAT 2025 论文）	v4（CP-Agent / ASP-Bench 方案）
执行者	宿主聊天大模型，通过 MCP 编辑工具	宿主大模型（或用于批量运行的 mcp-minion），作为求解器程序员
工作单元	模型项（add_item、solve_model 等）	完整、可运行的 Python 求解器程序
执行方式	在 MCP 服务内部	在持久化的 IPython 内核（ipython_mcp）中
验证方式	由宿主大模型手动完成	内置于循环中：运行 → 检查 → submit_code
产物	瞬态模型状态	经过验证、可重新执行的程序，可供保留
宿主接口	多个细粒度模型编辑工具	求解内核：select_backend、python_exec、submit_code
后端	MiniZinc、PySAT、MaxSAT、Z3、ASP	PySAT、MaxSAT、Z3、CPMpy、Clingo、DIDP

引用

• Stefan Szeider，《通过模型上下文协议连接语言模型与符号求解器》，SAT 2025。介绍 v3 架构（v3 分支）。 DOI 10.4230/LIPIcs.SAT.2025.30
• Stefan Szeider，《CP-Agent：Agent 式约束规划》，载于 第 3 届代码大模型国际研讨会（LLM4Code 2026）论文集，第 6–13 页，ACM，2026 年。介绍 v4 背后的 IPython 内核方案。 DOI 10.1145/3786181.3788711
• Stefan Szeider，《ASP-Bench：从自然语言到逻辑程序》，载于 2026 年 IEEE/ACM 第 2 届神经符号软件工程国际研讨会（NSE '26）论文集，第 1–8 页，ACM，2026 年。 介绍 v4 测试问题采用的验证门控基准测试方法。 DOI 10.1145/3786168.3788402

许可证

MIT；详见 LICENSE。