MCP 求解器

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

概述

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

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

有关 MCP 求解器 系统架构和理论基础的详细描述，请参阅附带的研究论文：Stefan Szeider, "MCP-Solver: Integrating Language Models with Constraint Programming Systems", arXiv:2501.00539, 2024.

可用工具

在下文中，item 指的是 (MiniZinc/PySat/Z3) 代码的某一部分，而 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]"  # Install all solvers

可用模式 / 求解后端

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 求解器包含一个用于开发、实验和诊断目的的 MCP 客户端，基于 ReAct 代理框架。该客户端作为 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 test-client --query <query_file>.md

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

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

示例

示例 1：选角问题（MiniZinc）

这是基于 George Johnson (NYT, 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）

用户

检查是否可以在 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文件。