mcp-solver

MCP 求解器

模型上下文协议 (MCP) 服务器向大型语言模型公开 SAT、SMT 和约束求解功能。

概述

MCP Solver通过模型上下文协议将 SAT、SMT 和约束求解与 LLM 集成，使 AI 模型能够以交互方式创建、编辑和求解：

• MiniZinc中的约束模型
• PySAT中的 SAT 模型
• Z3 Python中的 SMT 公式

有关MCP Solver 的系统架构和理论基础的详细描述，请参阅随附的研究论文：Stefan Szeider， “MCP-Solver：将语言模型与约束编程系统集成” ，arXiv:2501.00539，2024。

可用工具

以下， 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 。

快速入门：

可用模式/解决后端

MCP 求解器提供三种不同的运行模式，每种模式都集成了不同的约束求解后端。每种模式都需要特定的依赖项，并提供独特的功能来解决不同类型的问题。

MiniZinc 模式

MiniZinc 模式提供与 MiniZinc 约束建模语言的集成，具有以下特点：

• 具有全局约束的丰富约束表达
• 与 Chuffed 约束求解器集成
• 优化能力
• 通过get_solution访问解决方案值

依赖项：需要minizinc包（ uv pip install -e ".[mzn]" ）

配置：要在 MiniZinc 模式下运行，请使用：

PySAT 模式

PySAT 模式允许与 Python SAT 解决工具包进行交互，具有以下特点：

• 使用 CNF（合取范式）的命题约束建模
• 可以使用各种 SAT 解算器（Glucose3、Glucose4、Lingeling 等）
• 基数约束（at_most_k、at_least_k、exactly_k）
• 支持布尔约束求解

依赖项：需要python-sat包（ uv pip install -e ".[pysat]" ）

配置：要在 PySAT 模式下运行，请使用：

Z3 模式

Z3 模式提供对 Z3 SMT（可满足性模理论）求解功能的访问，具有以下特点：

• 丰富的类型系统：布尔值、整数、实数、位向量、数组
• 使用量词进行约束求解
• 优化能力
• 常见建模模式的模板库

依赖项：需要z3-solver包（ uv pip install -e ".[z3]" ）

配置：要在 Z3 模式下运行，请使用：

MCP 测试客户端

MCP Solver 包含一个基于ReAct代理框架的 MCP 客户端，用于开发、实验和诊断。该客户端充当 LLM 和 MCP 服务器之间的中介，有助于将自然语言问题陈述转换为形式化的约束编程解决方案。

安装

客户端需要 LLM 提供商提供的API 密钥。对于 Anthropic（默认 LLM 为 Claude Sonnet 3.7），请设置ANTHROPIC_API_KEY环境变量。您可以在自己的环境中设置该变量，也可以将其包含在项目根目录下的.env文件中。

用法

客户端为每个求解器后端提供专门的命令：

示例

示例 1：铸造问题（MiniZinc）

这是基于乔治·约翰逊 (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 扮演）满足所有约束。

示例 2：N 皇后问题 (MiniZinc)

用户

检查你是否能在 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 时仍可控制。

示例 3：旅行推销员问题 (MiniZinc)

用户

一位驻扎在维也纳的销售员需要规划她即将在奥地利的行程，每个省会城市各走一次。请帮忙找到最短路线。距离（公里）：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文件。