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

smt-sudoku-mcp

Jetzt können Ihre Agenten selbstbewusst Sudoku spielen!

Ein MCP-Server, der die Leistungsfähigkeit des Lösens von Satisfiability-Modulo-Theories (SMT) mithilfe von Z3 anhand des klassischen Constraint-Satisfaction-Rätsels Sudoku demonstriert.

Sudoku lässt sich sauber auf SMT-Primitive abbilden: Das Generieren eines Rätsels bedeutet, ein Modell zu finden, das die Sudoku-Beschränkungen erfüllt, und dann zu beweisen, dass eine reduzierte Menge an Hinweisen immer noch nur eine Lösung hat; das Validieren eines Gitters bedeutet, dieselben Beschränkungen gegen gegebene Zellwerte zu prüfen; das Lösen eines Rätsels bedeutet, ein Modell zu finden oder zu beweisen, dass keines existiert.

Werkzeuge

Alle vier Werkzeuge sind zustandslos: Jeder Aufruf nimmt ein vollständiges Gitter explizit entgegen und/oder gibt es zurück, ohne serverseitigen Sitzungszustand.

Ein Sudoku-Gitter wird als {"rows": [[...9 ints...], ...9 rows...]} dargestellt, wobei jede Zelle 1-9 für eine gegebene Ziffer oder 0 für eine leere Zelle ist. Jedes Werkzeugergebnis, das eine bestimmte Zelle (einen Konflikt) benennt, meldet row/col als 1-basiert, entsprechend der üblichen Beschreibung von Sudoku-Zellen im Text (Zeile 1, Spalte 1 ist die oberste linke Zelle).

generate_sudoku_puzzle

Generiert ein neues, eindeutig lösbares Sudoku-Rätsel.

• Eingabe: difficulty — eines von "easy", "medium" oder "hard" (Standard "medium"), das einer ungefähren Zielanzahl an Hinweisen entspricht.

• Ausgabe: {"puzzle": <grid>, "difficulty": <str>, "givens": <int>} — givens ist die tatsächliche Anzahl gefüllter Zellen, die leicht über dem Ziel liegen kann, wenn das Entfernen weiterer Zellen die Eindeutigkeit gebrochen hätte.

validate_partial_sudoku_solution

Prüft, ob ein teilweise gefülltes Gitter konfliktfrei ist und, falls ja, ob es noch vervollständigt werden kann.

• Eingabe: grid — ein teilweises Gitter (0 für leere Zellen).

• Ausgabe: {"has_conflicts": <bool>, "conflicts": [<cell>, ...], "is_completable": <bool | null>} — is_completable ist null, wenn Konflikte vorhanden sind, da die Vervollständigbarkeit keine sinnvolle Frage ist, bis diese behoben sind.

validate_full_sudoku_solution

Prüft, ob ein vollständig gefülltes Gitter eine korrekte Sudoku-Lösung ist.

• Eingabe: grid — erwartet keine leeren Zellen.

• Ausgabe: {"is_valid": <bool>, "has_empty_cells": <bool>, "conflicts": [<cell>, ...]}.

solve_sudoku_puzzle

Löst ein ungelöstes Gitter oder meldet, warum es nicht gelöst werden kann.

• Eingabe: grid — ein zu lösendes teilweises Gitter (0 für leere Zellen).

• Ausgabe: {"status": "satisfiable" | "conflicting_givens" | "unsatisfiable", "solution": <grid | null>, "conflicts": [<cell>, ...]}. conflicts ist nur gefüllt, wenn status "conflicting_givens" ist (zwei gegebene Zellen verletzen direkt eine Zeilen-/Spalten-/Box-Regel); "unsatisfiable" bedeutet, dass die gegebenen Zellen paarweise konfliktfrei sind, aber keine Vervollständigung existiert.

Related MCP server: Gurddy MCP Server

Installation

Erfordert Python 3.13+. Das Paket ist auf PyPI veröffentlicht.

Am einfachsten lässt es sich mit uvx ausführen, das das Paket bei der ersten Verwendung in eine temporäre Umgebung lädt und keinen separaten Installationsschritt erfordert:

uvx smt-sudoku-mcp

Alternativ installieren Sie es mit pip (oder uv pip) und führen das installierte Konsolenskript direkt aus:

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

Um am Quellcode selbst zu arbeiten statt am veröffentlichten Paket, siehe Entwicklung unten.

Verwendung mit einem MCP-Client

Dieser Server spricht standardmäßig MCP über stdio, sodass jeder MCP-Client, der einen Unterprozess starten kann, ihn ohne weitere Einrichtung verwenden kann. Setzen Sie stattdessen SMT_SUDOKU_MCP_TRANSPORT=streamable-http, wenn der Client einen eigenständigen HTTP-Dienst erreichen muss; siehe Konfiguration.

Claude Code

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

Claude Desktop

Fügen Sie einen Eintrag unter Einstellungen → Entwickler → Konfiguration bearbeiten (claude_desktop_config.json) hinzu:

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

Andere MCP-Clients und Agent-Frameworks

Jeder Client, der eine rohe MCP-Serverdefinition akzeptiert — Cursor, Windsurf, VS Code oder ein benutzerdefinierter Agent, der auf einem MCP-SDK basiert — kann dasselbe command/args-Paar verwenden: uvx und ["smt-sudoku-mcp"]. Für streamable-http führen Sie den Server separat mit SMT_SUDOKU_MCP_TRANSPORT=streamable-http uvx smt-sudoku-mcp aus und richten den Client auf http://<host>:<port>/mcp aus, anstatt ihm einen Befehl zum Starten zu geben.

Sobald die Verbindung hergestellt ist, kann ein Agent die vier oben genannten Werkzeuge wie jedes andere Werkzeug aufrufen. Wenn Sie beispielsweise einen Agenten bitten, „ein schweres Sudoku-Rätsel zu generieren, es dann zu lösen und die Lösung zu überprüfen“, werden generate_sudoku_puzzle, solve_sudoku_puzzle und validate_full_sudoku_solution ohne weitere Anleitung verkettet, da die Beschreibung und das Schema jedes Werkzeugs ausreichen, damit der Agent die Reihenfolge selbst planen kann.

Konfiguration

Umgebungsvariablen, alle optional:

Entwicklung

Um den Server aus einem Quellcode-Checkout statt aus dem veröffentlichten Paket auszuführen, verwenden Sie uv:

uv sync
uv run smt-sudoku-mcp

Siehe AGENTS.md für Architekturnotizen und den vollständigen Satz an Entwicklungskommandos (just -l).

Mitwirken

Issues und Pull-Requests sind willkommen.

Lizenz

MIT.