---

MCP 求解器

一个通过模型上下文协议（MCP）向大型语言模型提供 SAT、SMT 和约束求解能力的服务器。

---

概述

MCP 求解器 通过模型上下文协议将 SAT、SMT 和约束求解与大型语言模型集成，使 AI 模型能够交互式地创建、编辑和求解：

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

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

可用工具

以下内容中，item 指代 (MinZinc/Pysat/Z3) 代码的某一部分，model 指代编码。

工具名称	描述
clear_model	从模型中移除所有项
add_item	在特定索引处添加新项
delete_item	删除索引处的项
replace_item	替换索引处的项
get_model	获取当前模型内容（带编号的项）
solve_model	求解模型（带超时参数）

---

系统要求

• Python 和项目管理器 uv
• Python 3.11+
• 模式特定要求：MiniZinc、PySAT、Python Z3（所需包通过 pip 安装）
• 操作系统：macOS、Windows、Linux（需适当适配）

---

安装

MCP 求解器需要 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]"  # 安装所有求解器

---

可用模式 / 求解后端

MCP 求解器提供三种不同的操作模式，每种模式都与不同的约束求解后端集成。每种模式需要特定的依赖，并为解决不同类别的问题提供独特的功能。

MiniZinc 模式

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

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

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

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

mcp-solver-mzn

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 模式运行，请使用：

mcp-solver-pysat

Z3 模式

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

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

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

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

mcp-solver-z3

MCP 测试客户端

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

安装

# 安装客户端依赖
uv pip install -e ".[client]"

# 验证客户端安装和配置
uv run test-setup-client

客户端需要从 LLM 提供商获取 API 密钥。对于 Anthropic（默认 LLM 是 Claude Sonnet 3.7），设置 ANTHROPIC_API_KEY 环境变量。可以在环境中设置，也可以包含在项目根目录的 .env 文件中。

客户端还支持其他 LLM 提供商，包括 OpenAI、Google（Gemini）、OpenRouter，甚至通过 LM Studio 的本地模型。可以使用 --mc 命令行标志指定要使用的模型。有关模型代码格式的详细信息，请参阅 INSTALL.md。

使用

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

# MiniZinc 模式
uv run run-test mzn --problem <path/to/problem.md>

# PySAT 模式
uv run run-test pysat --problem <path/to/problem.md>

# Z3 模式
uv run run-test z3 --problem <path/to/problem.md>

---

示例

示例 1：选角问题（MiniZinc）

基于 George Johnson（《纽约时报》，1999 年 7 月 13 日）的示例。

用户

假设一位戏剧导演觉得有义务在他的作品中要么选他的女主角 Alvarez，要么选他的侄子 Cohen。但 Alvarez 小姐不会与 Cohen 先生（她的前情人）一起出演，她要求演员阵容中包括她的新欢 Davenport。制片人出于自己的考虑，坚持要求 Branislavsky 出演。但 Branislavsky 先生不会与 Alvarez 小姐或 Davenport 一起出演。导演能完成选角吗？

系统： clear_model

模型已清除

系统： add_item（多次）

var bool: alvarez;
var bool: cohen;
var bool: branislavsky;
var bool: davenport;
constraint alvarez \/ cohen;                          % 必须选 Alvarez 或 Cohen
constraint not (alvarez /\ cohen);                    % Alvarez 不会与 Cohen 一起工作
constraint alvarez -> davenport;                      % 如果 Alvarez 被选，Davenport 必须被选
constraint branislavsky;                              % Branislavsky 必须被选
constraint not (branislavsky /\ alvarez);             % Branislavsky 不会与 Alvarez 一起工作
constraint not (branislavsky /\ davenport);           % Branislavsky 不会与 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）

用户

检查是否可以在 n×n 的棋盘上放置 n 个皇后。尝试 n=10、20、30、40 并比较求解时间。

系统： clear_model

模型已清除

系统： 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.001s n=20: 0.005s n=30: 0.040s n=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 文件。