╭─╮╭┬╮╶┬╴   ╭─╮╷ ╷╶┬╮╭─╮╷╭ ╷ ╷
╰─╮│││ │    ╰─╮│ │ │││ │├┴╮│ │
╰─╯╵ ╵ ╵    ╰─╯╰─╯╶┴╯╰─╯╵ ╵╰─╯

smt-sudoku-mcp

现在，你的智能体可以自信地玩数独了！

一个 MCP 服务器，通过经典约束满足谜题数独，展示可满足性模理论（SMT）求解的强大能力，底层使用 Z3。

数独可以清晰地映射到 SMT 原语：生成谜题意味着找到一个满足数独约束的模型，然后证明一组缩减后的线索仍然只有一个解；验证网格意味着针对给定的单元格值检查这些相同的约束；求解谜题意味着找到一个模型或证明不存在任何模型。

工具

所有四个工具都是无状态的：每次调用都显式地接收和/或返回一个完整的网格，服务器端不保存任何会话状态。

数独网格表示为 {"rows": [[...9 个整数...], ...9 行...]}，其中每个单元格为 1-9 表示已给出的数字，或 0 表示空单元格。任何引用特定单元格（冲突）的工具结果都会以 1 为起始索引报告 row/col，这与数独单元格在文本中的常规描述方式一致（第 1 行第 1 列是左上角单元格）。

generate_sudoku_puzzle

生成一个新的、具有唯一解的数独谜题。

• 输入： difficulty — "easy"、"medium" 或 "hard" 之一（默认 "medium"），对应一个近似的目标线索数量。

• 输出： {"puzzle": <grid>, "difficulty": <str>, "givens": <int>} — givens 是实际填充的单元格数量，如果进一步移除单元格会破坏唯一性，则该数量可能略高于目标值。

validate_partial_sudoku_solution

检查一个部分填充的网格是否无冲突，如果是，则检查它是否仍然可以完成。

• 输入： grid — 部分网格（空单元格为 0）。

• 输出： {"has_conflicts": <bool>, "conflicts": [<cell>, ...], "is_completable": <bool | null>} — 当存在冲突时，is_completable 为 null，因为在冲突解决之前，可完成性不是一个有意义的问题。

validate_full_sudoku_solution

检查一个完全填充的网格是否是正确的数独解。

• 输入： grid — 预期没有空单元格。

• 输出： {"is_valid": <bool>, "has_empty_cells": <bool>, "conflicts": [<cell>, ...]}。

solve_sudoku_puzzle

求解一个未完成的网格，或报告无法求解的原因。

• 输入： grid — 待求解的部分网格（空单元格为 0）。

• 输出： {"status": "satisfiable" | "conflicting_givens" | "unsatisfiable", "solution": <grid | null>, "conflicts": [<cell>, ...]}。conflicts 仅在 status 为 "conflicting_givens" 时填充（两个已给出的单元格直接违反行/列/宫规则）；"unsatisfiable" 表示给出的线索两两之间无冲突，但不存在任何完成方案。

Related MCP server: Gurddy MCP Server

安装

需要 Python 3.13+。该包已发布在 PyPI 上。

最简单的运行方式是使用 uvx，它会在首次使用时将包获取到临时环境中，无需单独的安装步骤：

uvx smt-sudoku-mcp

或者，使用 pip（或 uv pip）安装它，然后直接运行已安装的控制台脚本：

pip install smt-sudoku-mcp
smt-sudoku-mcp

如果想直接处理源代码而不是已发布的包，请参阅下面的开发部分。

与 MCP 客户端一起使用

此服务器默认通过 stdio 进行 MCP 通信，因此任何能够启动子进程的 MCP 客户端都可以直接使用它，无需额外设置。如果客户端需要连接独立的 HTTP 服务，请改为设置 SMT_SUDOKU_MCP_TRANSPORT=streamable-http；请参阅配置。

Claude Code

claude mcp add smt-sudoku -- uvx smt-sudoku-mcp

Claude Desktop

在设置 → 开发者 → 编辑配置（claude_desktop_config.json）下添加一个条目：

{
  "mcpServers": {
    "smt-sudoku": {
      "command": "uvx",
      "args": ["smt-sudoku-mcp"]
    }
  }
}

其他 MCP 客户端和智能体框架

任何接受原始 MCP 服务器定义的客户端——Cursor、Windsurf、VS Code，或基于 MCP SDK 构建的自定义智能体——都可以使用相同的 command/args 组合：uvx 和 ["smt-sudoku-mcp"]。对于 streamable-http，请使用 SMT_SUDOKU_MCP_TRANSPORT=streamable-http uvx smt-sudoku-mcp 单独运行服务器，并将客户端指向 http://<host>:<port>/mcp，而不是给它一个要启动的命令。

连接后，智能体可以像调用任何其他工具一样调用上述四个工具。例如，让智能体"生成一个困难数独谜题，然后求解并检查解"将自动串联 generate_sudoku_puzzle、solve_sudoku_puzzle 和 validate_full_sudoku_solution，无需进一步指导，因为每个工具的描述和模式足以让智能体自行规划执行顺序。

配置

环境变量，全部可选：

开发

要从源代码检出而不是已发布的包运行服务器，请使用 uv：

uv sync
uv run smt-sudoku-mcp

有关架构说明和完整的开发命令列表（just -l），请参阅 AGENTS.md。

贡献

欢迎提交 issue 和 pull request。

许可证

MIT。