AI导哈

约束求解器

MCP Solver 是一个通过模型上下文协议（MCP）将约束求解、SAT、SMT和ASP能力暴露给大型语言模型的服务器，适用于需要符号推理和约束解决的复杂问题场景。

  • by JunseokTheLee
  • Python
  • 本地部署
  • 更新于
在 GitHub 查看 JunseokTheLee/MCPSolver-Eval

使用说明

MCP求解器

一种模型上下文协议（MCP）服务器，向大型语言模型公开约束求解、SAT、SMT和ASP功能。

概述

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

关于 MCP求解器 系统架构和理论基础，见随附的研究论文：Stefan Szeider， “通过模型上下文协议连接语言模型和符号求解器”，坐2025。

可用工具

接下来， 项目 指（MiniZinc/PySAT/Z3/ASP）代码的某些部分，以及 模型 到编码。

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

系统要求

  • Python和项目经理 紫外线
  • Python 3.11+
  • 特定模式要求：MiniZinc、PySAT、Python Z3（所需软件包通过pip安装）
  • 操作系统：macOS、Windows、Linux（经过适当调整）

安装

MCP求解器需要Python 3.11+ uv 包管理器和求解器特定依赖关系（MiniZinc、Z3或PySAT）。

有关Windows、macOS和Linux的详细安装说明，请参阅 安装.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、玲玲等）
  • 基数约束（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求解器包括一个用于开发、实验和诊断目的的MCP客户端，基于 交互式推理与行动 代理框架。该客户端充当LLM和MCP服务器之间的中介，促进自然语言问题语句转换为形式约束编程解决方案。

安装

# Install client dependencies
uv pip install -e ".[client]"

# Verify client installation and configuration
uv run test-setup-client

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

该客户端还支持其他LLM提供商，包括OpenAI、谷歌（Gemini）、OpenRouter，甚至通过LM Studio支持本地模型。您可以指定使用哪个模型 --mc 命令行标志。看 安装.md 有关模型代码格式的详细信息。

用法

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

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

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

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

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

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

例子

示例1：铸造问题（MiniZinc）

这是基于乔治·约翰逊的一个例子（纽约时报，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-Queens问题（MiniZinc）

用户

检查你是否可以把n个皇后放在nxn棋盘上。尝试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.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}

最佳路线：维也纳→ 圣波尔滕→ Linz → 萨尔茨堡→ 布雷根茨→ 因斯布鲁克→ 克拉根福→ Graz → 艾森施塔特→ 维也纳，全长1564公里。

反馈

您可以通过以下方式向作者提供反馈 形式.

免责声明

此MCP求解器处于原型阶段，应谨慎使用。鼓励用户进行实验，但在关键环境中的任何使用都是他们自己的风险。

许可证

此项目根据MIT许可证获得许可-请参阅 许可证 文件以获取详细信息。

相关 MCP