模型上下文协议 (MCP) 服务器向大型语言模型公开 SAT、SMT 和约束求解功能。
MCP Solver通过模型上下文协议将 SAT、SMT 和约束求解与 LLM 集成，使 AI 模型能够以交互方式创建、编辑和求解：
有关MCP Solver 的系统架构和理论基础的详细描述，请参阅随附的研究论文：Stefan Szeider， “MCP-Solver：将语言模型与约束编程系统集成” ，arXiv:2501.00539，2024。
Related MCP server: mcp-optimizer
以下， item指的是（MinZinc/Pysat/Z3）代码的某些部分， model指的是编码。
工具名称 | 描述 |
| 从模型中移除所有项目 |
| 在特定索引处添加新项目 |
| 删除索引处的项目 |
| 替换索引处的项目 |
| 获取带有编号项目的当前模型内容 |
| 解决模型（带超时参数） |
Python 和项目经理uv
Python 3.11+
模式特定要求：MiniZinc、PySAT、Python Z3（所需软件包通过 pip 安装）
操作系统：macOS、Windows、Linux（经过适当调整）
MCP Solver 需要 Python 3.11+、 uv包管理器和求解器特定的依赖项（MiniZinc、Z3 或 PySAT）。
有关 Windows、macOS 和 Linux 的详细安装说明，请参阅INSTALL.md 。
快速入门：
git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate
uv pip install -e ".[all]" # Install all solversMCP 求解器提供三种不同的运行模式，每种模式都集成了不同的约束求解后端。每种模式都需要特定的依赖项，并提供独特的功能来解决不同类型的问题。
MiniZinc 模式提供与 MiniZinc 约束建模语言的集成，具有以下特点：
具有全局约束的丰富约束表达
与 Chuffed 约束求解器集成
优化能力
通过get_solution访问解决方案值
依赖项：需要minizinc包（ uv pip install -e ".[mzn]" ）
配置：要在 MiniZinc 模式下运行，请使用：
mcp-solver-mznPySAT 模式允许与 Python SAT 解决工具包进行交互，具有以下特点：
使用 CNF（合取范式）的命题约束建模
可以使用各种 SAT 解算器（Glucose3、Glucose4、Lingeling 等）
基数约束（at_most_k、at_least_k、exactly_k）
支持布尔约束求解
依赖项：需要python-sat包（ uv pip install -e ".[pysat]" ）
配置：要在 PySAT 模式下运行，请使用：
mcp-solver-pysatZ3 模式提供对 Z3 SMT（可满足性模理论）求解功能的访问，具有以下特点：
丰富的类型系统：布尔值、整数、实数、位向量、数组
使用量词进行约束求解
优化能力
常见建模模式的模板库
依赖项：需要z3-solver包（ uv pip install -e ".[z3]" ）
配置：要在 Z3 模式下运行，请使用：
mcp-solver-z3MCP Solver 包含一个基于ReAct代理框架的 MCP 客户端，用于开发、实验和诊断。该客户端充当 LLM 和 MCP 服务器之间的中介，有助于将自然语言问题陈述转换为形式化的约束编程解决方案。
# Install client dependencies
uv pip install -e ".[client]"
# Verify client installation and configuration
uv run test-setup-client客户端需要 LLM 提供商提供的API 密钥。对于 Anthropic（默认 LLM 为 Claude Sonnet 3.7），请设置ANTHROPIC_API_KEY环境变量。您可以在自己的环境中设置该变量，也可以将其包含在项目根目录下的.env文件中。
客户端为每个求解器后端提供专门的命令：
# MiniZinc mode
uv run run-test mzn --problem <path/to/problem.md>
# PySAT mode
uv run run-test pysat --problem <path/to/problem.md>
# Z3 mode
uv run run-test z3 --problem <path/to/problem.md>这是基于乔治·约翰逊 (George Johnson) 的一个例子 (纽约时报，1999 年 7 月 13 日)。
用户
假设一位戏剧导演觉得有义务在一部作品中安排他那位才华横溢的女演员阿尔瓦雷斯或他的侄子演员科恩出演。但阿尔瓦雷斯小姐不愿与科恩先生（她以前的情人）同台演出，并要求演员阵容中必须包括她的新欢演员达文波特。制片人为了报答自己的恩惠，坚持要让演员布拉尼斯拉夫斯基出演。但布拉尼斯拉夫斯基先生不愿与阿尔瓦雷斯小姐或达文波特先生同台演出。导演能安排这部戏的演员吗？
系统： clear_model
Model cleared
系统： add_item （多个）
var bool: alvarez; var bool: cohen; var bool: branislavsky; var bool: davenport; constraint alvarez \/ cohen; % Must cast either Alvarez or Cohen constraint not (alvarez /\ cohen); % Alvarez won't work with Cohen constraint alvarez -> davenport; % If Alvarez is cast, Davenport must be cast constraint branislavsky; % Branislavsky must be cast constraint not (branislavsky /\ alvarez); % Branislavsky won't work with Alvarez constraint not (branislavsky /\ davenport); % Branislavsky won't work with Davenport solve satisfy;
系统： solve_model
{'status': 'SAT', 'solution': Solution(alvarez=False, cohen=True, branislavsky=True, davenport=False, _checker=''), 'solve_time': 0.0}
该解决方案（由 Cohen 和 Branislavsky 扮演，但不由 Alvarez 或 Davenport 扮演）满足所有约束。
用户
检查你是否能在 nxn 的棋盘上放置 n 个皇后。尝试 n=10,20,30,40，并比较解题时间
系统： clear_model
Model cleared
系统： add_item （多个）
int: n = 10; array[1..n] of var 1..n: queens; constraint alldifferent(queens); constraint alldifferent([queens[i] + i | i in 1..n]); constraint alldifferent([queens[i] - i | i in 1..n]); solve satisfy;
系统： solve_model （通过改变 n 的值，n=10、20、30 和 40）
求解时间比较：n=10: 0.001sn=20: 0.005sn=30: 0.040sn=40: 0.043s
所有测试棋盘尺寸均有解决方案。时间复杂度呈非线性增长，但在 n=40 时仍可控制。
用户
一位驻扎在维也纳的销售员需要规划她即将在奥地利的行程，每个省会城市各走一次。请帮忙找到最短路线。距离（公里）：1=维也纳，2=圣珀尔滕，3=艾森施塔特，4=林茨，5=格拉茨，6=克拉根福，7=萨尔茨堡，8=因斯布鲁克，9=布雷根茨
[用户消息中提供的距离矩阵表]
系统： add_item （多个）
include "globals.mzn"; int: n = 9; array[1..n,1..n] of int: dist = [|0,65,60,184,195,319,299,478,631|65,0,125,119,130,254,234,413,566|60,125,0,184,157,281,261,440,593|184,119,184,0,208,252,136,315,468|195,130,157,208,0,136,280,459,629|319,254,281,252,136,0,217,391,566|299,234,261,136,280,217,0,188,343|478,413,440,315,459,391,188,0,157|631,566,593,468,629,566,343,157,0|]; array[1..n] of var 1..n: succ; var int: total_dist = sum(i in 1..n)(dist[i,succ[i]]); constraint circuit(succ); solve minimize total_dist;
系统： solve_model
{'status': 'SAT', 'solution': Solution(objective=1564, succ=[2, 4, 1, 7, 3, 5, 9, 6, 8], _checker=''), 'solve_time': 0.002}
最佳路线：维也纳→圣珀尔滕→林茨→萨尔茨堡→布雷根茨→因斯布鲁克→克拉根福→格拉茨→艾森斯塔特→维也纳，总距离1,564公里。
您可以通过此表格向作者提供反馈。
此 MCP 求解器尚处于原型阶段，应谨慎使用。鼓励用户进行实验，但在关键环境中使用需自行承担风险。
该项目根据 MIT 许可证获得许可 - 有关详细信息，请参阅LICENSE文件。
Execute Python code in the persistent solving kernel.
Runs in the kernel set up by select_backend unless kernel_id overrides it. State persists across calls (variables, imports). Raise timeout (seconds, max 300) for long solver runs.
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes | ||
| timeout | No | ||
| kernel_id | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations, so the description carries the full burden. It usefully discloses that state (variables, imports) persists across calls and that timeout caps at 300 seconds, but says nothing about error behavior, sandboxing, or how execution output is captured/returned.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Four short lines, purpose front-loaded, with each remaining sentence adding a distinct operational fact (kernel source, state persistence, timeout cap). No filler or restated name text.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
No output schema exists, yet the description never describes what an execution returns (stdout, errors, result value), which is a meaningful gap for a code-execution tool. Kernel selection, persistence, and timeout behavior are covered, so the definition is workable but not complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate, and it does for two of three params: kernel_id is explained as overriding the kernel established by select_backend, and timeout is defined in seconds with a max of 300. The 'code' param is left implicit but is self-evident from the tool purpose.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb+resource ('Execute Python code') and adds the key qualifier that it runs in the persistent solving kernel, which differentiates it from a one-shot execution. It references select_backend for kernel setup, but never contrasts itself with submit_code, so sibling distinction is only partial.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Gives implied usage guidance: raise the timeout for long solver runs, and rely on state persisting across calls. However, it never says when to prefer this over submit_code or when to instead use python_interrupt/python_reset, so the caller must infer routing.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Interrupt running code in the solving kernel (state is preserved).
| Name | Required | Description | Default |
|---|---|---|---|
| kernel_id | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It does disclose one meaningful trait — that state is preserved rather than discarded — but says nothing about what happens if nothing is running, whether interruption is cooperative, permissions, or the result of the call.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single front-loaded sentence with no filler; the verb and effect lead the reader immediately. It is efficient, though it is arguably too terse for the behavioral gaps it leaves.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a one-parameter tool with no output schema and no annotations, the description covers purpose and one behavioral note. It omits how to target a specific kernel and what the caller observes after interrupting, leaving the agent to guess at invocation details.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
One parameter (kernel_id, nullable, default null) has 0% schema description coverage, and the description adds no meaning: it never explains what kernel_id identifies, that it is optional, or what the default targets. The 'solving kernel' phrasing hints at a default target but is not tied to the parameter.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb ('interrupt') and resource ('running code in the solving kernel'), plus a scope qualifier ('state is preserved') that separates it from python_reset. It does not name siblings explicitly, so the differentiation is inferable rather than stated.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied by the verb: call it when running code needs to be stopped without losing kernel state. There is no explicit guidance on when to prefer this over python_reset, nor any prerequisite or condition (e.g., only valid while execution is in flight).
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Create a new kernel (no kernel_id) or reset one (with kernel_id).
Prefer select_backend, which installs the right solver packages for you. The kernel created or reset here becomes the target of bare python_exec calls.
| Name | Required | Description | Default |
|---|---|---|---|
| packages | No | ||
| kernel_id | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the behavioral burden. It usefully discloses that the created or reset kernel becomes the target of bare python_exec calls, but it does not mention that resetting may discard existing kernel state, nor does it explain the packages parameter's effect.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is three short sentences with no wasted text. The main behavior is front-loaded, followed by the alternative tool guidance and the downstream effect on python_exec.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a two-parameter, state-changing tool with no annotations, no output schema, and 0% schema description coverage, the description is incomplete. It covers purpose and one parameter but leaves packages undocumented and does not describe reset side effects or state loss.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate for both parameters. It explains kernel_id's effect well by describing create-without vs reset-with, but it completely omits the packages parameter, leaving half the parameters undocumented.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description gives a specific verb and resource, and it clearly distinguishes the two modes: no kernel_id creates a new kernel, while a provided kernel_id resets one. It also names the related sibling tool select_backend, so the tool's role is immediately identifiable.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
It explicitly says to prefer select_backend when solver packages are needed, which is useful routing guidance. The create-vs-reset condition is also clear, though the description does not explicitly state when not to use python_reset or what prerequisites exist.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Check kernel state: active kernels, defined variables, packages.
| Name | Required | Description | Default |
|---|---|---|---|
| kernel_id | No |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden of behavioral disclosure. 'Check' implies a read-only operation, but it does not explicitly state that it is non-destructive, nor does it describe side effects, authorization needs, or rate limits. It only lists what is inspected, which is minimal behavioral context.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single, front-loaded sentence with no filler. It efficiently conveys the core purpose in one clause.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a simple no-required-parameter tool with no output schema, the description gives an outline of what is returned (kernels, variables, packages). However, it omits usage context and parameter semantics, leaving gaps an agent must infer.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The schema has 0% description coverage and the description never mentions the optional kernel_id parameter. It does not explain what the parameter does, when to supply it, or what the default behavior is when omitted.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb 'Check' and resource 'kernel state', and enumerates the inspected items (active kernels, variables, packages). It is clear but does not differentiate this tool from siblings like python_exec or python_interrupt.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No when-to-use guidance is given. The description does not say when to prefer this over python_exec or python_interrupt, nor does it state any prerequisites like requiring an active kernel.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Start solving a constraint problem: call this FIRST, once per problem.
Sets up a persistent IPython kernel preloaded with the backend's solver library and helper functions, and returns the modeling instructions for that backend. Calling it again recycles the kernel for a new problem (previous session state is cleared).
Backends:
pysat: Boolean satisfiability — feasibility, combinatorial search
maxsat: weighted optimization over Boolean constraints
z3: SMT — integers/reals/bitvectors, proofs, program verification
cpmpy: finite-domain constraint programming — scheduling, assignment, puzzles
clingo: Answer Set Programming — logic rules, defaults, reachability
didp: dynamic programming (state-space search) — routing, sequencing, packing
Unsure which backend fits? Read the resource mcp-solver://guide first.
Then iterate with python_exec (write, run, verify against the problem statement), and finish by calling submit_code with the final, verified, self-contained program. UNSAT / "no solution exists" is a valid outcome.
| Name | Required | Description | Default |
|---|---|---|---|
| solver | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden and delivers: persistent kernel lifetime, that re-invocation clears previous session state, that it returns modeling instructions, and that UNSAT is a legitimate terminal outcome. These are exactly the behavioral traits an agent needs and that the schema does not express.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Front-loaded imperative first sentence, then setup behavior, then the backend list, then the workflow tail. The bulleted backend table is dense with information and every line earns its place; no filler.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
No output schema exists, but the description says what is returned (modeling instructions) and sketches the full three-stage workflow ending in submit_code. For a single-parameter entry-point tool, an agent has everything required to select and invoke it correctly.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0% and the single 'solver' parameter has no enum, so the description must supply the value domain — and it does, enumerating all six backends with a one-line semantic gloss each (e.g. 'z3: SMT — integers/reals/bitvectors, proofs, program verification'). It does not explicitly state that these strings are the accepted values of the solver argument, so the mapping is inferred rather than stated.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
Specific verb+resource: 'Start solving a constraint problem' and sets up a persistent IPython kernel preloaded with the backend solver library. It explicitly positions itself against siblings by naming the full workflow (python_exec to iterate, submit_code to finish), so an agent can place it without opening other schemas.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Explicit when-to-use ('call this FIRST, once per problem'), re-use semantics ('Calling it again recycles the kernel for a new problem'), an escape hatch for uncertainty ('Unsure which backend fits? Read the resource mcp-solver://guide first'), and the follow-on tools. Nothing is left to inference.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Submit the final, verified, self-contained solver program.
Call ONCE at the end, only after executing the program via python_exec and passing your verification. The code is syntax-checked; on success it is stored and linked as a resource (the server keeps the last 50).
| Name | Required | Description | Default |
|---|---|---|---|
| code | Yes |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden and does well: it discloses validation behavior (syntax-checked), the failure path, and what happens on success (stored and linked as a resource, server retains the last 50). It omits whether resubmission overwrites a prior submission and what an error response looks like.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Three short sentences, front-loaded with the action and artifact, then the timing constraint, then the side effect. No filler and nothing repeated from the schema.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a single-parameter submission tool with no annotations and no output schema, the description covers purpose, timing, validation, and persistence/retention. Remaining gaps (retry semantics, error format) are minor given the tool's simplicity.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 0% and the schema itself only says 'code: string', so the description has to define the payload; it does so by specifying the code must be the final, verified, self-contained solver program. It stops short of stating language/format constraints, but the payload's required qualities are communicated.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb (submit) plus the exact resource (the final, verified, self-contained solver program), which is distinct from the sibling execution/status tools. It does not explicitly name which sibling it is contrasted with, but the artifact it accepts is unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
Gives explicit timing ('Call ONCE at the end'), an explicit prerequisite ('only after executing the program via python_exec and passing your verification'), and names the sibling tool involved. An agent cannot mistake when this should fire.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v4.1.0python_execpython_interruptpython_resetpython_statusselect_backendsubmit_codeScored across 6 tools
Most tools are clearly distinct: python_status, python_interrupt, python_exec, and submit_code each have a unique role. The only mild overlap is between select_backend and python_reset (both create/configure kernels), but descriptions explicitly steer users to prefer select_backend, resolving the ambiguity.
Four tools share a consistent python_<action> prefix (python_status, python_interrupt, python_exec, python_reset), but select_backend and submit_code break this pattern with a verb_noun convention. Two coexisting conventions make it mixed but still readable.
Six tools is well-scoped for a constraint-solving workflow: backend setup, execution, kernel management, and final submission. Each tool earns its place with no redundancy.
The lifecycle (select_backend -> python_exec iterate -> submit_code, with status/interrupt/reset for kernel control) is well covered. Minor gaps: no tool to list or retrieve previously submitted solutions (only a resource mention), but core workflows are complete.
A comprehensive Model Context Protocol (MCP) server that enables AI assistants to interact with yo…
A Model Context Protocol server for Wix AI tools
MCP server for progressive tool usage at any scale (see https://klavis.ai)
