Awesome MCP › Other MCP Servers

szeider/mcp-solver

⭐ 183 Python added to this list on 2025-05-14 repository created 2024-12-14

MCP Solver is a Python MCP server that turns the connected LLM host into a solver-writing agent for combinatorial and constraint problems. Rather than solving anything itself, the server hands the host a toolkit. The select_backend tool starts a persistent IPython kernel preloaded with the solver library and helper functions for the chosen backend and returns that backend's modeling instructions; calling it again recycles the kernel for the next problem. Kernel tools (python_exec, python_reset, python_status, python_interrupt) let the host write, run and verify a real solver program step by step. The submit_code tool is the finish line: the final self-contained program is syntax-checked and, on success, stored and linked back as an MCP resource, with the verdict returned as structured content. Two resources are exposed, a guide covering backend selection and workflow, and per-solver templates holding the full modeling instructions. Six backends are supported: pysat for Boolean satisfiability, maxsat for weighted optimization, z3 for SMT solving and verification, cpmpy for constraint programming, clingo for answer set programming, and didp for domain-independent dynamic programming, which suits routing, sequencing, scheduling and packing. Solver libraries are injected at solve time with uv run --with instead of being installed into the host environment, keeping each solve reproducible. The server runs over stdio, needs no API key and works with any MCP host such as Claude Desktop, Claude Code or Cursor, because the model doing the solving belongs to the host. An optional statistics file logs one JSON line per solving episode with tool-call counts, execution failures, submissions and wall time. A command-line path runs the same pipeline without an MCP host through mcp-minion, a minimal ReAct agent over MCP developed in the same repository, which needs an OpenRouter key. Version 4 re-architected both the MCP interface and the solving engine; the earlier SAT 2025 paper design remains on the v3 branch. Requires Python 3.13 and uv.

https://github.com/szeider/mcp-solver

mcpmcp-serverconstraint-solvingsatsmtoptimizationpythonz3clingo