smt-sudoku-mcp

Now, your agents can play Sudoku confidently!

An MCP server that demonstrates the power of satisfiability modulo theories (SMT) solving, using Z3, through the classic constraint-satisfaction puzzle of Sudoku.

Sudoku maps cleanly onto SMT primitives: generating a puzzle means finding a model that satisfies the Sudoku constraints and then proving a reduced set of clues still has only one solution; validating a grid means checking those same constraints against given cell values; solving a puzzle means finding a model or proving none exists.

As of 1.0.0, the four tools' input/output schemas below are a stable public contract: any breaking change to them will be called out explicitly in CHANGELOG.md and reflected in a major version bump.

Tools

All four tools are stateless: every call takes and/or returns a complete grid explicitly, with no server-side session state.

A Sudoku grid is represented as {"rows": [[...9 ints...], ...9 rows...]}, where each cell is 1-9 for a given digit or 0 for an empty cell. Any tool result that names a specific cell (a conflict) reports row/col as 1-indexed, matching how Sudoku cells are conventionally described in text (row 1, column 1 is the top-left cell).

generate_sudoku_puzzle

Generates a new, uniquely-solvable Sudoku puzzle.

• Input: difficulty — one of "very easy", "easy", "medium", "hard", or "very hard" (default "medium"), mapping to an approximate target clue count: 63, 51, 42, 30, and 21 respectively. "very hard"'s target of 21 sits just above the proven minimum of 17 givens for any uniquely-solvable Sudoku puzzle, so in practice it commonly lands noticeably above 21 (e.g. mid-20s), since removal stops once no further cell can be cleared without breaking uniqueness.
• Output: {"puzzle": <grid>, "difficulty": <str>, "givens": <int>} — givens is the actual number of filled cells, which may be slightly above the target if removing further cells would have broken uniqueness.

validate_partial_sudoku_solution

Checks whether a partially-filled grid is conflict-free and, if so, whether it can still be completed.

• Input: grid — a partial grid (0 for empty cells).
• Output: {"conflicts": [<cell>, ...], "is_completable": <bool | null>, "empty_cells": [<cell>, ...], "has_conflicts": <bool>, "empty_cells_count": <int>} — is_completable is null when conflicts are present, since completability is not a meaningful question until they are resolved. empty_cells lists every still-empty cell regardless of has_conflicts; empty_cells_count is len(empty_cells).

validate_full_sudoku_solution

Checks whether a fully-filled grid is a correct Sudoku solution.

• Input: grid — expected to have no empty cells.
• Output: {"has_empty_cells": <bool>, "conflicts": [<cell>, ...], "is_valid": <bool>}.

solve_sudoku_puzzle

Solves an unsolved grid, or reports why it cannot be solved.

• Input: grid — a partial grid to solve (0 for empty cells).
• Output: {"status": "satisfiable" | "conflicting_givens" | "unsatisfiable", "solution": <grid | null>, "conflicts": [<cell>, ...]}. conflicts is only populated when status is "conflicting_givens" (two given cells directly violate a row/column/box rule); "unsatisfiable" means the givens are pairwise conflict-free but no completion exists.

Installation

Requires Python 3.13+. The package is published on PyPI.

The simplest way to run it is with uvx, which fetches the package into an ephemeral environment on first use and requires no separate install step:

uvx smt-sudoku-mcp

Alternatively, install it with pip (or uv pip) and run the installed console script directly:

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

To work on the source itself rather than the published package, see Development below.

Using it with an MCP client

This server speaks MCP over stdio by default, so any MCP client that can launch a subprocess can use it without further setup. Set SMT_SUDOKU_MCP_TRANSPORT=streamable-http instead if the client needs to reach a standalone HTTP service; see Configuration.

Claude Code

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

Claude Desktop

Add an entry under Settings → Developer → Edit Config (claude_desktop_config.json):

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

Other MCP clients and agent frameworks

Any client that accepts a raw MCP server definition — Cursor, Windsurf, VS Code, or a custom agent built on an MCP SDK — can use the same command/args pair: uvx and ["smt-sudoku-mcp"]. For streamable-http, run the server separately with SMT_SUDOKU_MCP_TRANSPORT=streamable-http uvx smt-sudoku-mcp and point the client at http://<host>:<port>/mcp rather than giving it a command to launch.

Once connected, an agent can call the four tools above as it would any other tool. For example, asking an agent to "generate a hard Sudoku puzzle, then solve it and check the solution" will chain generate_sudoku_puzzle, solve_sudoku_puzzle, and validate_full_sudoku_solution without further guidance, since each tool's description and schema are sufficient for the agent to plan the sequence itself.

Configuration

Environment variables, all optional:

The server has no built-in authentication or authorization of its own: SMT_SUDOKU_MCP_ALLOWED_ORIGINS and the request guard it feeds protect against spoofed browser origins and DNS-rebinding-style attacks, not against an arbitrary network client calling its tools. There is no scope for adding authentication — this server is intended to be run on a local machine or an otherwise trusted network, never exposed directly to an untrusted network.

Development

To run the server from a source checkout instead of the published package, use uv:

uv sync
uv run smt-sudoku-mcp

See AGENTS.md for architecture notes and the full set of development commands (just -l).

Contributing

Issues and pull requests are welcome; see CONTRIBUTING.md. See CONTRIBUTORS.md for the list of contributors, and CHANGELOG.md for the release history.

Security

See SECURITY.md for the vulnerability disclosure policy.

License

MIT.