MCP Solver

MCP Solver

site icon
2025.04.16 54
Python约束求解逻辑推理优化问题开发效率
MCP Solver 是一个基于 Model Context Protocol (MCP) 的服务,旨在将 SAT、SMT 和约束求解能力集成到大型语言模型 (LLMs) 中。它允许 AI 模型通过 MCP 协议交互式地创建、编辑和求解各种约束模型,包括 MiniZinc、PySAT 和 Z3 Python 的模型。该服务特别适用于需要复杂逻辑推理和约束求解的场景,如排班问题、路径优化和逻辑谜题等。
View on GitHub

Overview

基本能力

产品定位

MCP Solver 是一个专为大型语言模型设计的约束求解服务,通过 MCP 协议提供 SAT、SMT 和约束求解能力。

核心功能

  • 支持 MiniZinc、PySAT 和 Z3 Python 三种求解后端
  • 提供模型编辑功能(添加、删除、替换模型项)
  • 支持模型求解并返回解决方案
  • 包含 MCP 测试客户端,用于开发和诊断

适用场景

  • 排班问题(如演员选角)
  • 组合优化问题(如 N-皇后问题)
  • 路径规划问题(如旅行商问题)
  • 逻辑谜题求解

工具列表

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

常见问题解答

  • 需要 Python 3.11+ 和 uv 包管理器
  • 不同求解模式需要安装特定依赖
  • 测试客户端需要 LLM API 密钥(默认使用 Anthropic Claude)

使用教程

使用依赖

  • Python 3.11+
  • 项目管理器 uv
  • 模式特定依赖:
  • MiniZinc 模式:minizinc
  • PySAT 模式:python-sat
  • Z3 模式:z3-solver

安装教程

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

调试方式

  1. 安装客户端依赖:
uv pip install -e ".[client]"
uv run test-setup-client
  1. 运行测试客户端:
# 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

许可证

该项目遵循 MIT 开源许可条款,请参阅 MIT 了解完整条款。