制約解法用のMCPサーバー(SA、MAXSAT、SMT、CP、ASP、DP)。回転します 接続されたLLMホストをソルバー作成エージェントに変換します:ホストはPythonを受け取ります カーネルには実ソルバーライブラリがあらかじめインストールされており、 選択されたバックエンドとサブミッションゲート。ホストが問題をエンコードし、実行します そしてそれを実ソルバーと照合して検証し、最終的なプログラムを提出します — 結果は解と、生成された検証済みソルバープログラムです それ。

バージョン4は完全なアーキテクチャ再構築です。 MCPインターフェースおよび 解>エンジンが変わりました。SAT 2025のペーパー(v3)の設計は今も生き続けています

v3 枝。 以下の「バージョン3からバージョン4まで」を参照してください。

MCPサーバー

mcp-solver-serveはstdioを上書き、任意のMCPホストと連携します:Claude デスクトップ、Claude Code、カーソル、または自分のクライアントで。ホストのLLMは 自らを解く — サーバーはソルバーツールキットです。LLMを実行しず、必要なものです APIキーなし:

• select_backend(solver) は バックエンドのソルバーライブラリとヘルパー関数、そしてモデリングを返します そのバックエンドの命令を再度呼び出すと、カーネルは の 次の問題。

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"]
    }
  }
}