Example MCP server: smt-sudoku-mcp

smt-sudoku-mcp is an MCP server that demonstrates the power of satisfiability modulo theories (SMT) solving, using Z3, through the classic constraint-satisfaction puzzle of Sudoku. Unlike pymcp, it exposes tools only, with no prompts, resources or resource templates, so this example shows the mcpdocs::tools directive on its own.

The project is available on GitHub at smt-sudoku-mcp.

MCP artefacts

• Tools
  • generate_sudoku_puzzle
  • validate_partial_sudoku_solution
  • validate_full_sudoku_solution
  • solve_sudoku_puzzle