---

MCP 求解器

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

---

概述

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

• MiniZinc 中的约束模型
• PySAT 中的 SAT 模型
• PySAT 中的 MaxSAT 优化问题
• Z3 Python 中的 SMT 公式
• Clingo 中的答案集程序

有关 MCP 求解器 系统架构和理论基础的详细描述，请参阅随附的研究论文：Stefan Szeider, "通过模型上下文协议桥接语言模型和符号求解器", SAT 2025。

可用工具

以下内容中，item 指的是（MiniZinc/PySAT/Z3/ASP）代码的某一部分，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

MaxSAT 模式

MaxSAT 模式提供了对 PySAT 优化问题的专门支持，具有以下功能：

• 支持加权合取范式（WCNF）
• 与 RC2 MaxSAT 求解器集成
• 具有目标跟踪的优化能力
• 支持硬约束和软约束

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

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

mcp-solver-maxsat

Z3 模式

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

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

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

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

mcp-solver-z3

ASP 模式

ASP（答案集编程）模式提供了与 ASP 求解器（如 Clingo）的集成，用于通过逻辑程序进行声明式问题求解。功能包括：

• 用于组合和知识表示问题的表达性逻辑编程
• 支持约束、选择规则、聚合和优化语句
• 与 Clingo 求解器集成以高效计算答案集
• 访问答案集和模型检查

依赖项：需要 clingo 包（uv pip install -e ".[asp]" 或包含在 [all] 中）

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

mcp-solver-asp

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>

# MaxSAT 模式
uv run run-test maxsat --problem <path/to/problem.md>

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

# ASP 模式
uv run run-test asp --problem <path/to/problem.md>

---

示例

示例 1：选角问题（MiniZinc）

这是基于 George Johnson（纽约时报，1999 年 7 月 13 日）的一个示例。

用户

假设一位戏剧导演觉得有义务在他的作品中选角，要么是他的新星 Actress Alvarez，要么是他的侄子 Actor Cohen。但 Alvarez 小姐不会与 Cohen 先生（她的前情人）同台演出，她要求演员阵容包括她的新欢 Actor Davenport。制片人为了还自己的人情，坚持让 Actor 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）

用户

检查是否可以在 nxn 的棋盘上放置 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文件。

---