MCP-сервер для решения ограничений (SAT, MaxSAT, SMT, CP, ASP, DP). Он поворачивается связанный LLM-хост становится агентом для записи решателя: хост получает Python Ядро предварительно загружено с библиотекой Real Solver, моделирующей инструкции для выбранный бэкэнд и элемент подачи данных. Хост кодирует задачу, запускается и проверяет её с реальным решателем, и отправляет финальную программу — Результатом является решение плюс проверенная программа решателя, которая создала Это.

Версия 4 — это полная реархитектура. Как интерфейс MCP, так и решающий механизм изменился; дизайн из статьи SAT 2025 (v3) продолжает существовать без изменений на ветка v3. См. ниже раздел с v3 по v4.

Сервер MCP

mcp-solver-serve работает через stdio и работает с любым ведущим MCP: Claude Рабочий стол, Claude Code, Cursor или ваш собственный клиент. Хост-LLM выполняет решающий сам себя — сервер — это набор инструментов для решателей; он не запускает LLM и требует Нет ключа API:

• select_backend(solver) устанавливает персистентное ядро IPython с Библиотека решателей и вспомогательные функции бэкенда, а также возвращает моделирование инструкции для этого бэкенда. Повторный вызов перерабатывает ядро для Следующая проблема.

MCP Solver

An MCP server for constraint solving (SAT, MaxSAT, SMT, CP, ASP, DP). It turns the connected LLM host into a solver-writing agent: the host gets a Python kernel preloaded with a real solver library, modeling instructions for the chosen backend, and a submission gate. The host encodes the problem, runs and verifies it against the real solver, and submits the final program — the outcome is the solution plus the verified solver program that produced it.

Version 4 is a complete re-architecture. Both the MCP interface and the solving engine changed; the design from the SAT 2025 paper (v3) lives on unchanged on the v3 branch. See From v3 to v4 below.

The MCP server

mcp-solver-serve runs over stdio and works with any MCP host: Claude Desktop, Claude Code, Cursor, or your own client. The host LLM does the solving itself — the server is a solver toolkit; it runs no LLM and needs no API key:

• select_backend(solver) sets up a persistent IPython kernel with the backend’s solver library and helper functions, and returns the modeling instructions for that backend. 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; bare python_exec calls are routed to the solving kernel automatically.
• submit_code(code) is the finish line: the final self-contained program is syntax-checked and, on success, stored and linked back as an MCP resource (mcp-solver://submissions/{id}), with the verdict as structured content.
• Resources: mcp-solver://guide (backend selection and workflow) and mcp-solver://template/{solver} (the full modeling instructions, browsable without selecting).
• Statistics (optional): set MCP_SOLVER_STATS=/path/to/stats.jsonl in the server’s env to log one JSON line per solving episode — tool-call counts, execution failures, submissions, wall time. Host tokens are invisible to the server by protocol design; tool usage is the comparable metric across hosts. (submit_code results also carry a compact stats snapshot as structured content; the CLI path reports tokens and actual OpenRouter cost via --stats-json.)

Claude Desktop configuration, from a checkout (the working setup today, and the development path always; see Installation):

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uv",
      "args": ["run", "--project", "/path/to/mcp-solver", "--extra", "agent", "mcp-solver-serve"]
    }
  }
}