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

smt-sudoku-mcp

これで、あなたのエージェントも自信を持って数独を解けるようになります！

Z3 を用いて、充足可能性モジュロ理論（SMT）ソルビングの威力を、古典的な制約充足パズルである数独を通して実演する MCP サーバーです。

数独は SMT のプリミティブにきれいにマッピングできます。パズルを生成するということは、数独の制約を満たすモデルを見つけ、さらに削減された手がかりのセットが依然として唯一の解を持つことを証明することを意味します。グリッドを検証するということは、与えられたセルの値に対して同じ制約をチェックすることを意味します。パズルを解くということは、モデルを見つけるか、存在しないことを証明することを意味します。

ツール

4 つのツールはすべてステートレスです。各呼び出しは完全なグリッドを明示的に受け取り、および/または返します。サーバー側のセッション状態はありません。

数独グリッドは {"rows": [[...9 ints...], ...9 rows...]} として表され、各セルは与えられた数字の場合は 1〜9、空のセルの場合は 0 です。特定のセル（競合）を指定するツールの結果は、row/col を 1 始まりで報告します。これは、数独のセルがテキストで慣例的に記述される方法（行 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" の場合のみ設定されます（2 つの与えられたセルが行/列/ボックスのルールに直接違反している場合）。"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 にポイントします。

接続後、エージェントは他のツールと同様に上記の 4 つのツールを呼び出すことができます。たとえば、エージェントに「難しい数独パズルを生成して、それを解いて、解を検証して」と依頼すると、generate_sudoku_puzzle、solve_sudoku_puzzle、validate_full_sudoku_solution が追加の指示なしで連鎖します。各ツールの説明とスキーマが、エージェントがシーケンスを自分で計画するのに十分だからです。

設定

環境変数（すべてオプション）:

開発

公開パッケージではなくソースチェックアウトからサーバーを実行するには、uv を使用します。

uv sync
uv run smt-sudoku-mcp

アーキテクチャのメモと開発コマンドの完全なセット（just -l）については、AGENTS.md を参照してください。

貢献

Issue とプルリクエストを歓迎します。

ライセンス

MIT。