mcp-z3-prover

Name: mcp-z3-prover
Author: daedalus

本地服务

github.com/daedalus科研与教育127 周前更新

代码仓库

关于 mcp-z3-prover

mcp-z3-prover 将 Z3 求解器 API 封装为 MCP 服务，供客户端构建约束问题、求解或优化，并查看变量取值。

主要功能

01创建布尔、整数和实数变量
02添加求解器约束
03求解约束问题
04优化目标
05读取模型值并列出变量
06重置求解器状态

适用场景

01用变量和约束描述问题
02求解整数或实数约束
03优化求解目标
04查看解的取值或重启求解器

MCP 相关

它向 MCP 客户端提供 Z3 工具，用于创建变量、管理约束、求解、优化、检查模型及重置状态。

配置

本地服务的配置在各客户端中通用，复制后粘贴到客户端的 MCP 配置文件即可。

mcp.json · 通用配置

{
  "mcpServers": {
    "daedalus-mcp-z3-prover": {
      "command": "uvx",
      "args": [
        "mcp-z3-prover"
      ]
    }
  }
}

启动命令uvx mcp-z3-prover

本地服务需要在你的电脑上安装运行环境（如 Node.js 18+）。各客户端的配置文件位置不同，请参考客户端文档。

安装包

pypimcp-z3-prover0.1.0stdio

工具

收录的工具列表 · 更新于 2 周前

参数	类型	必填	说明
name	string	是

详细介绍

mcp-z3-prover

提供 Z3 求解器 API 的 MCP 服务

安装

pip install mcp-z3-prover

使用

from mcp_z3_prover import mcp

# Run the server
mcp.run()

或从命令行运行：

mcp-z3-prover

MCP 工具

该服务提供以下工具：

create_bool_var - 创建布尔变量
create_int_var - 创建整数变量
create_real_var - 创建实数变量
create_int_constant - 创建整数常量
create_real_constant - 创建实数常量
add_constraint - 向求解器添加约束
solve - 求解当前问题
get_model_value - 获取模型中变量的值
optimize - 按优化目标求解
reset_solver - 重置求解器状态
list_variables - 列出所有已创建的变量

示例

# Create variables
create_int_var("x")
create_int_var("y")

# Add constraints
add_constraint("int:x + int:y == 10")
add_constraint("int:x > 0")
add_constraint("int:y > 0")

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"x": "5", "y": "5"}}

# Get specific values
x_val = get_model_value("int:x")

整数因式分解示例

# Factor n = 4295229443 where n = p * q with q <= sqrt(n)
create_int_var("p")
create_int_var("q")

# Add constraints
add_constraint("int:p * int:q == 4295229443")
add_constraint("4295229443 > int:p")
add_constraint("4295229443 > int:q")
add_constraint("int:q <= 65537")  # sqrt(4295229443) ≈ 65537
add_constraint("int:q > 1")
add_constraint("int:p > 1")
add_constraint("int:q % 2 != 0")  # q is odd
add_constraint("int:p % 2 != 0")  # p is odd

# Solve
result = solve()
# Returns: {"status": "sat", "model": {"p": "65539", "q": "65537"}}
# Verification: 65537 * 65539 = 4295229443

开发

git clone https://github.com/daedalus/mcp-z3-prover.git
cd mcp-z3-prover
pip install -e ".[test]"

# run tests
pytest

# format
ruff format src/ tests/

# lint
ruff check src/ tests/

# type check
mypy src/