mcp-solver

------

# MCP Solver

[![MCP 兼容](https://img.shields.io/badge/MCP-Compatible-green.svg)](https://modelcontextprotocol.io/) [![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](https://opensource.org/licenses/MIT) [![Python 版本](https://img.shields.io/badge/Python-3.11%2B-blue.svg)](https://www.python.org/)

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

------

## 概述

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

- [MiniZinc](https://www.minizinc.org/) 中的约束模型
- [PySAT](https://pysathq.github.io/) 中的 SAT 模型
- [Z3 Python](https://ericpony.github.io/z3py-tutorial/guide-examples.htm) 中的 SMT 公式

有关 *MCP Solver* 系统架构和理论基础的详细描述，请参阅随附的研究论文：Stefan Szeider, ["MCP-Solver: Integrating Language Models with Constraint Programming Systems"](https://arxiv.org/abs/2501.00539), arXiv:2501.00539, 2024.

## 可用工具

在下文中，*item* 指的是 (MinZinc/Pysat/Z3) 代码的某个部分，而 *model* 指的是编码。

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

------

## 系统要求

- Python 和项目管理器 [uv](https://docs.astral.sh/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](INSTALL.md)。

快速开始：
```bash
git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate
uv pip install -e ".[all]"  # 安装所有求解器

---

可用模式 / 求解后端

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

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（Satisfiability Modulo Theories）求解能力的访问，具有以下功能：

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

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

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

mcp-solver-z3

MCP 测试客户端

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

安装

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

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

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

用法

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

# MiniZinc 模式
uv run test-client --query <query_file>.md

# PySAT 模式
uv run test-client-pysat --query <query_file>.md

# Z3 模式
uv run test-client-z3 --query <query_file>.md

---

示例

示例 1：选角问题 (MiniZinc)

这基于 George Johnson (NYT, July 13, 1999) 的一个例子。

用户

假设一位戏剧导演觉得有义务在他的制作中选角他的天真女演员 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)

用户

检查是否可以在 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 Solver 处于原型阶段，应谨慎使用。 鼓励用户进行实验，但在关键环境中的任何使用均由他们自己承担风险。

---

许可证

本项目根据 MIT 许可证获得许可 - 有关详细信息，请参阅 LICENSE 文件。

---