제약 해석을 위한 MCP 서버(SAT, MaxSAT, SMT, CP, ASP, DP). 회전합니다 연결된 LLM 호스트를 솔버 작성 에이전트로 연결: 호스트는 파이썬을 받습니다 커널은 실수 해석기 라이브러리가 미리 로드되어 있으며, 모델링 명령어를 수행합니다. 선택한 백엔드와 제출 게이트를 사용합니다. 호스트가 문제를 인코딩하고 실행합니다 그리고 이를 실제 해법자와 대조하여 검증하고, 최종 프로그램을 제출한다 — 결과는 해와 생성된 검증된 해법 프로그램입니다 그것.

버전 4는 완전한 재아키텍처입니다. MCP 인터페이스와 해법 엔진이 변경되었습니다; SAT 2025 시험지(v3)의 설계는 계속 이어지고 있습니다 변경 사항이 없습니다 v3 지부. 아래> '버전 3부터 버전 4까지’를 참고하세요.

MCP 서버

mcp-solver-serve는 stdio를 실행하며 MCP 호스트와 함께 작동합니다: Claude 데스크톱, Claude 코드, 커서, 또는 본인의 클라이언트 중 하나를 사용할 수 있습니다. 호스트 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"]
    }
  }
}